From 99826cb11dc8478b1c9bf7c0f7116e621e8618cb Mon Sep 17 00:00:00 2001
From: notin
Date: Tue, 26 Jan 2010 15:22:51 +0000
Subject: make init + NMake.v/NMake_gen.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12690 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile        | 2 +-
 Makefile.build  | 2 +-
 Makefile.common | 6 ++++++
 3 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/Makefile b/Makefile
index c96577651c..14e5827008 100644
--- a/Makefile
+++ b/Makefile
@@ -88,7 +88,7 @@ export GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \
   scripts/tolink.ml kernel/copcodes.ml
 export GENMLIFILES:=$(YACCFILES:.mly=.mli)
 export GENHFILES:=kernel/byterun/coq_jumptbl.h
-export GENVFILES:=theories/Numbers/Natural/BigN/NMake.v
+export GENVFILES:=theories/Numbers/Natural/BigN/NMake_gen.v
 export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) $(GENVFILES)
 export MLFILES  := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml'  ')' $(FIND_PRINTF_P) | \
   while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \
diff --git a/Makefile.build b/Makefile.build
index 864f6f27bf..7d63e33b0c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -796,7 +796,7 @@ plugins/%_mod.ml: plugins/%.mllib
 	$(HIDE)$(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4USE) $<` `$(CAMLP4DEPS) $<` $(CAMLP4COMPAT) -impl $< > $@ \
 	  || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
-%.vo %.glob: %.v states/initial.coq $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
+%.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d  $(VO_TOOLS_ORDER_ONLY)
 	$(SHOW)'COQC      $<'
 	$(HIDE)rm -f $*.glob 
 	$(HIDE)$(BOOTCOQTOP) -compile $*
diff --git a/Makefile.common b/Makefile.common
index a1bfd08856..de84aaefe3 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -204,6 +204,12 @@ else
  PLUGINSOPT:=
 endif
 
+ifeq ($(BEST),opt)
+  INITPLUGINSBEST:=$(INITPLUGINSOPT)
+else
+  INITPLUGINSBEST:=$(INITPLUGINS)
+endif
+
 CMA:=$(CLIBS) $(CAMLP4OBJS)
 CMXA:=$(CMA:.cma=.cmxa)
 
-- 
cgit v1.2.3