From: Richard W.M. Jones <rjones@redhat.com>
Date: Wed, 8 Jan 2020 16:18:38 +0000 (+0000)
Subject: build: Remove man/*.? man pages when running 'make clean'.
X-Git-Tag: v'0.2'~60
X-Git-Url: http://git.annexia.org/?p=goals.git;a=commitdiff_plain;h=b88599eb9c51240065878c8556976dc1cd805137

build: Remove man/*.? man pages when running 'make clean'.

Fixes commit abfde4ea239de6b9458243a862d5da0302a241a4.
---

diff --git a/Goalfile.in b/Goalfile.in
index b865c9c..39a9587 100644
--- a/Goalfile.in
+++ b/Goalfile.in
@@ -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.