build: Remove man/*.? man pages when running 'make clean'.
[goals.git] / Goalfile.in
index 75ce273..39a9587 100644 (file)
@@ -37,7 +37,7 @@ goal clean = {
         popd
     done
     rm -f src/parser.ml src/parser.mli src/lexer.ml src/parser.conflicts
-    rm -f docs/*.1
+    rm -f man/*.1 man/*.5
 
     # We don't delete src/goals because it is required to do builds.
     # If you want to really delete it, use the maintainer-clean rule.
@@ -110,7 +110,9 @@ goal depend =
 
 let POD2MAN = "@POD2MAN@"
 
-goal documentation = : pod2man ("goals", "1")
+goal documentation = : pod2man ("goals", "1"),
+                       pod2man ("Goalfile", "5"),
+                       pod2man ("goals-reference", "5")
 
 goal pod2man (page, section) =
 "man/%page.%section" : "docs/%page.pod" {