diff options
| author | filliatr | 2001-07-17 07:09:49 +0000 |
|---|---|---|
| committer | filliatr | 2001-07-17 07:09:49 +0000 |
| commit | faa7694e94139b74590fae09c6806c16de4069e4 (patch) | |
| tree | 427c137e92d3b235a875fcf2cc7cd96e337f5041 /tools | |
| parent | 0fb97de232866adbec1d7eb14e33fa4a7b15fc31 (diff) | |
"make clean" nettoie les .g all.ps all-gal.ps et les fichiers HTML
générés à partir des .v
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1856 85f007b7-540e-0410-9357-904b9bb8a0f7
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; |