diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 9f1e178a55..d22072cd35 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -109,7 +109,8 @@ let standard sds = print "\t$(COQBIN)coq_makefile -f Make -o Makefile\n"; print "\n"; print "clean:\n"; - print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *~\n"; + print "\trm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~\n"; + print "\trm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)\n"; List.iter (fun x -> print "\t(cd "; print x; print " ; $(MAKE) clean)\n") sds; |