From b88599eb9c51240065878c8556976dc1cd805137 Mon Sep 17 00:00:00 2001 From: "Richard W.M. Jones" Date: Wed, 8 Jan 2020 16:18:38 +0000 Subject: [PATCH] build: Remove man/*.? man pages when running 'make clean'. Fixes commit abfde4ea239de6b9458243a862d5da0302a241a4. --- Goalfile.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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. -- 1.8.3.1