diff options
| author | letouzey | 2010-03-04 16:18:11 +0000 |
|---|---|---|
| committer | letouzey | 2010-03-04 16:18:11 +0000 |
| commit | b1edecb1b38df8a88552aa4251982238b3c3125d (patch) | |
| tree | 5389cb05198071483d7cad7771b638d7a780a5b9 /Makefile | |
| parent | 139bf11029dc16bf95c56646c41457b14cc35fdc (diff) | |
Makefile: make devdocclean was not removing *.dep.ps, btw let's remove *.dep.ps for svn
the syntax for find is sooo intuitive ...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12835 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -180,7 +180,7 @@ endif #GOTO_STAGE # Cleaning ########################################################################### -.PHONY: clean objclean cruftclean indepclean archclean ml4clean clean-ide ml4depclean depclean distclean cleanconfig cleantheories docclean devdocclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean doclean archclean optclean clean-ide ml4clean ml4depclean depclean cleanconfig distclean voclean devdocclean clean: objclean cruftclean depclean docclean devdocclean @@ -256,7 +256,7 @@ voclean: find theories plugins test-suite -name '*.vo' -o -name '*.glob' | xargs rm -f devdocclean: - find . -name '*.dep.ps' -o -name '*.dot' -exec rm -f {} \; + find . -name '*.dep.ps' -o -name '*.dot' | xargs rm -f ########################################################################### # Emacs tags |