aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorlmamane2008-02-13 16:32:07 +0000
committerlmamane2008-02-13 16:32:07 +0000
commitded46fc00ee76c3f2568619e1a48034b5865a8f2 (patch)
tree814abf51952b8fda2f002cd76ebd4dc3f6936f2c /Makefile
parentca4775a3b2cfdc0ab3ae12f453892a82aec048b1 (diff)
Implement KEEP_ML4_PREPROCESSED option in build system
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10561 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile6
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index 0da3ac0914..be1ee4ef26 100644
--- a/Makefile
+++ b/Makefile
@@ -112,10 +112,10 @@ ifdef CM_STAGE1
$(CAML_OBJECT_PATTERNS): always
$(call stage-template,1)
-%.ml4.preprocessed: stage1
+%.ml4-preprocessed: stage1
$(call stage-template,2)
else
-$(CAML_OBJECT_PATTERNS) %.ml4.preprocessed: stage1
+$(CAML_OBJECT_PATTERNS) %.ml4-preprocessed: stage1
$(call stage-template,2)
endif
@@ -177,7 +177,7 @@ clean-ide:
rm -f ide/utf8_convert.ml
ml4clean:
- rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4.preprocessed)
+ rm -f $(ML4FILESML) $(ML4FILESML:.ml=.ml4-preprocessed)
ml4depclean:
find . -name '*.ml4.d' | xargs rm -f