diff options
| author | letouzey | 2012-10-23 18:06:26 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-23 18:06:26 +0000 |
| commit | bdc7217d03a109a9149d7c93bbe2f95b1df480f5 (patch) | |
| tree | e5629f161ca05baa15552fc7cc06539777d9219b /Makefile.build | |
| parent | 40b00efff7e47b22c80c677514f9d689c918383c (diff) | |
Coqmktop: missing -I (fix #2851)
The modules used in coqmktop's temporary main file should have
their .cmi in the search path, hence a small set of -I is required:
lib, toplevel. We do not place their the full list to avoid issues
with the win32 command-line length
Btw, coqmktop -boot now also builds its list of -I instead of receiving
them via its command-line, it's simpler this way...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15926 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index 44be3c3d0c..c3768528ed 100644 --- a/Makefile.build +++ b/Makefile.build @@ -102,7 +102,6 @@ HIDE := $(if $(VERBOSE),,@) LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) -COREMLINCLUDES=$(addprefix -I , $(CORESRCDIRS)) -I $(MYCAMLP4LIB) OCAMLC := $(TYPEREX) $(OCAMLC) $(CAMLFLAGS) OCAMLOPT := $(TYPEREX) $(OCAMLOPT) $(CAMLFLAGS) @@ -222,7 +221,7 @@ minibyte: $(COQTOPBYTE) pluginsbyte ifeq ($(BEST),opt) $(COQTOPEXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -opt $(COREMLINCLUDES) $(OPTFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(STRIP) $@ else $(COQTOPEXE): $(COQTOPBYTE) @@ -231,7 +230,7 @@ endif $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(SHOW)'COQMKTOP -o $@' - $(HIDE)$(COQMKTOP) -boot -top $(COREMLINCLUDES) $(BYTEFLAGS) -o $@ + $(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ LOCALCHKLIBS:=$(addprefix -I , $(CHKSRCDIRS) ) CHKLIBS:=$(LOCALCHKLIBS) -I $(MYCAMLP4LIB) |