From ac98362d168bc96433bf09ced8ee992bce76483e Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 20 Sep 2012 17:25:20 +0000
Subject: Remove broken makefile option NO_RECOMPILE_LIB

 The idea was to allow rebuilding coqtop without the whole stdlib,
 but it's not working anymore since the stdlib also depends on
 plugins .cmxs, hence its compilation will be triggered anyway.

 Since I've no idea how to restore the old behavior (except via
 hacking the output of coqdep with more ORDER_ONLY hack), I simply
 declare this option dead, and remove it for improving clarity.

 NB: an imperfect workaround is to touch all the .vo after rebuilding
 coqtop and the plugins...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15823 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build | 12 ++----------
 1 file changed, 2 insertions(+), 10 deletions(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index 9d9f08ea07..bea461131c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -67,7 +67,6 @@ ALLDEPS:=$(addsuffix .d, \
 
 VERBOSE=
 NO_RECOMPILE_ML4=
-NO_RECOMPILE_LIB=
 NO_RECALC_DEPS=
 READABLE_ML4=	# non-empty means .ml of .ml4 will be ascii instead of binary
 VALIDATE=
@@ -151,13 +150,6 @@ endif
 ifdef VALIDATE
  VO_TOOLS_DEP += $(CHICKEN)
 endif
-ifdef NO_RECOMPILE_LIB
- VO_TOOLS_ORDER_ONLY:=$(VO_TOOLS_DEP)
- VO_TOOLS_STRICT:=
-else
- VO_TOOLS_ORDER_ONLY:=
- VO_TOOLS_STRICT:=$(VO_TOOLS_DEP)
-endif
 
 ifdef NO_RECALC_DEPS
   D_DEPEND_BEFORE_SRC:=|
@@ -471,7 +463,7 @@ pluginsopt: $(PLUGINSOPT)
 # rules to make theories and plugins
 ###########################################################################
 
-theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_STRICT) | theories/Init/%.v.d $(VO_TOOLS_ORDER_ONLY)
+theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP) | theories/Init/%.v.d
 	$(SHOW)'COQC -noinit $<'
 	$(HIDE)rm -f theories/Init/$*.glob
 	$(HIDE)$(BOOTCOQC) theories/Init/$* -noinit
@@ -894,7 +886,7 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(CAMLP4O) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@; \
 	else echo $< : Dependency $${DEPS} not ready yet; false; fi
 
-%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
+%.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d
 	$(SHOW)'COQC      $<'
 	$(HIDE)rm -f $*.glob 
 	$(HIDE)$(BOOTCOQC) $*
-- 
cgit v1.2.3