public / ack.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 8c20d51)
improved the "clean" entry
authorceriel <none@none>
Wed, 25 Mar 1987 22:48:25 +0000 (22:48 +0000)
committerceriel <none@none>
Wed, 25 Mar 1987 22:48:25 +0000 (22:48 +0000)
doc/Makefile patch | blob | history

diff --git a/doc/Makefile b/doc/Makefile
index e72a3ab..7ff0537 100644 (file)
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -64,4 +64,5 @@ opr:
                make pr | opr
 
 clean:
-               -rm -f *.old $(RESFILES) *.t *.out
+               -rm -f *.old $(RESFILES) *.t *.out LLgen.doc top.doc \
+                       occam.doc ego.doc
Unnamed repository; edit this file 'description' to name the repository.