aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorletouzey2009-03-16 13:41:49 +0000
committerletouzey2009-03-16 13:41:49 +0000
commitd63dee24c817560a6fea49dfe0c851b4df25ecf7 (patch)
tree8616d535967062650f2b2f1c61bc2aff810cc666 /Makefile
parentc4fc3d3d4bcad5fd6dbca6f55dffd20580006f35 (diff)
coqdep_boot: a specialized and dependency-free coqdep for killing one of the build stages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11984 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile12
1 files changed, 4 insertions, 8 deletions
diff --git a/Makefile b/Makefile
index b3be1e8138..a502ffbc90 100644
--- a/Makefile
+++ b/Makefile
@@ -27,7 +27,7 @@
# Specific command-line options to this Makefile
#
-# make GOTO_STAGE=N # perform only stage N (with N=1,2,3)
+# make GOTO_STAGE=N # perform only stage N (with N=1,2)
# make VERBOSE=1 # restore the raw echoing of commands
# make NO_RECALC_DEPS=1 # avoid recomputing dependencies
# make NO_RECOMPILE_LIB=1 # a coqtop rebuild does not trigger a stdlib rebuild
@@ -155,7 +155,7 @@ config/Makefile Makefile.common Makefile.build Makefile: ;
$(call stage-template,$(GOTO_STAGE))
else
-.PHONY: stage1 stage2 stage3 world revision
+.PHONY: stage1 stage2 world revision
stage1 $(STAGE1_TARGETS) : always
$(call stage-template,1)
@@ -163,14 +163,10 @@ stage1 $(STAGE1_TARGETS) : always
stage2 $(STAGE2_TARGETS) : stage1
$(call stage-template,2)
-stage3 $(STAGE3_TARGETS) : stage2
- $(call stage-template,3)
-
# Nota:
-# - world is one of the targets in $(STAGE3_TARGETS), hence launching
-# "make" or "make world" leads to recursion into stage{1,2,3}
+# - world is one of the targets in $(STAGE2_TARGETS), hence launching
+# "make" or "make world" leads to recursion into stage1 then stage2
# - the aim of stage1 is to build grammar.cma and q_constr.cmo
-# - the aim of stage2 is to build coqdep
# More details in dev/doc/build-system*.txt