diff options
| author | glondu | 2010-06-02 16:25:48 +0000 |
|---|---|---|
| committer | glondu | 2010-06-02 16:25:48 +0000 |
| commit | 791db4ddbf69e3fa0465dfb379fc7aec3630d9c6 (patch) | |
| tree | 023cfe05a48b84fc32203ecad93e1fe1e2b121b9 | |
| parent | 3d087f91ea9a9ca6ca7bfbac15763624f547f851 (diff) | |
Do not link system library into installed .cma
Linking a system library into a .cma can lead to some system module
(such as Unix) being linked twice in an executable, resulting in
possibly hard-to-debug errors.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13054 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index 192092e4e4..b23772dc02 100644 --- a/Makefile.build +++ b/Makefile.build @@ -649,7 +649,7 @@ dev/printers.cma: | dev/printers.mllib.d $(HIDE)$(OCAMLC) $(BYTEFLAGS) $(SYSCMA) $^ -o test-printer @rm -f test-printer $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $^ -linkall -a -o $@ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ parsing/grammar.cma: | parsing/grammar.mllib.d $(SHOW)'Testing $@' @@ -657,7 +657,7 @@ parsing/grammar.cma: | parsing/grammar.mllib.d $(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) -I $(CAMLLIB) unix.cma $^ -impl" -impl test.ml4 -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' - $(HIDE)$(OCAMLC) $(BYTEFLAGS) unix.cma $^ -linkall -a -o $@ + $(HIDE)$(OCAMLC) $(BYTEFLAGS) $^ -linkall -a -o $@ # toplevel/mltop.ml4 (ifdef Byte) @@ -800,7 +800,7 @@ plugins/%_mod.ml: plugins/%.mllib $(HIDE)\ DEPS=$(CAMLP4DEPS); \ if ls $${DEPS} > /dev/null 2>&1; then \ - $(CAMLP4O) $(PR_O) $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< $(TOTARGET); \ + $(CAMLP4O) $(PR_O) -I $(CAMLLIB) unix.cma $${DEPS} $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< $(TOTARGET); \ else echo $< : Dependency $${DEPS} not ready yet; false; fi %.vo %.glob: %.v states/initial.coq $(INITPLUGINSBEST) $(VO_TOOLS_STRICT) | %.v.d $(VO_TOOLS_ORDER_ONLY) |