aboutsummaryrefslogtreecommitdiff
path: root/Makefile.stage2
diff options
context:
space:
mode:
authorletouzey2010-03-04 16:18:35 +0000
committerletouzey2010-03-04 16:18:35 +0000
commita3fda4aa95b125545e1b64a57a56a20861dc0aa5 (patch)
tree353fc42a152f3456ca50c4eacb529d0fb6d90469 /Makefile.stage2
parent9ece79aa913d30adf14597f2eeec702e58240db9 (diff)
Makefile: no more separate stages
- Instead of the separate stage mechanism, we let make handle the build and inclusion of all .d. Some initial calls to camlp4o will fail, but make tries again later, and this finally works great. These initial error message are made nice to avoid bad interaction with M-x next-error - The only recursive call to a sub-make is Makefile calling Makefile.build in which the includes of .d take place. This allows to avoid compiling anything for a make clean or make tags git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12839 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.stage2')
-rw-r--r--Makefile.stage223
1 files changed, 0 insertions, 23 deletions
diff --git a/Makefile.stage2 b/Makefile.stage2
deleted file mode 100644
index e6a61b8e44..0000000000
--- a/Makefile.stage2
+++ /dev/null
@@ -1,23 +0,0 @@
-#######################################################################
-# v # The Coq Proof Assistant / The Coq Development Team #
-# <O___,, # INRIA-Rocquencourt & LRI-CNRS-Orsay #
-# \VV/ #############################################################
-# // # This file is distributed under the terms of the #
-# # GNU Lesser General Public License Version 2.1 #
-#######################################################################
-
-include Makefile.stage1
-include Makefile.doc
-
-STAGE2_DEPS := $(addsuffix .d, $(GENPLUGINSMOD) $(GENML4FILES) $(VFILES))
-
-.SECONDARY: $(STAGE2_DEPS)
--include $(STAGE2_DEPS)
-
-# NB: all $(STAGE1_DEPS) are already included thanks to the inclusion of
-# Makefile.stage1
-
-# For emacs:
-# Local Variables:
-# mode: makefile
-# End: