aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-07-12 16:28:10 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-07-12 16:28:10 +0200
commit72d9bf028d0cf40cb6c727c69bfbcc15aafc4944 (patch)
tree4f06742ac395a8021f1a371798f8a6a2330a6384
parent3a3f11fe1b6c0f059cf2bd0d71aa4deb4a876b26 (diff)
Makefile: no more .ml4.d hence no more rule to clean them
-rw-r--r--Makefile5
1 files changed, 1 insertions, 4 deletions
diff --git a/Makefile b/Makefile
index 3b9d1e67c..34ce67b7d 100644
--- a/Makefile
+++ b/Makefile
@@ -159,7 +159,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ;
# Cleaning
###########################################################################
-.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean ml4depclean depclean cleanconfig distclean voclean devdocclean
+.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean devdocclean
clean: objclean cruftclean depclean docclean devdocclean
@@ -220,9 +220,6 @@ clean-ide:
ml4clean:
rm -f $(GENML4FILES)
-ml4depclean:
- find . -name '*.ml4.d' | xargs rm -f
-
depclean:
find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f