aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorherbelin2004-07-19 09:38:39 +0000
committerherbelin2004-07-19 09:38:39 +0000
commit35ad1640ca69dbc257787c4eae6602582e54454c (patch)
tree208a55ff13511ca0ab565d25cba75be6f4c2ad5f
parent448fee159c56b0bc81679d53b8731913ea069376 (diff)
Indépendance de parser vis a vis de ocamlrun
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5955 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 78655a4372..dac013941f 100644
--- a/Makefile
+++ b/Makefile
@@ -673,7 +673,7 @@ PARSERCMX= $(PARSERREQUIRESCMX) $(PARSERCODE:.cmo=.cmx)
bin/parser$(EXE): $(PARSERCMO)
$(SHOW)'OCAMLC -o $@'
- $(HIDE)$(OCAMLC) -linkall -cclib -lunix $(OPTFLAGS) -o $@ \
+ $(HIDE)$(OCAMLC) -linkall -custom -cclib -lunix $(OPTFLAGS) -o $@ \
dynlink.cma $(CMA) $(PARSERCMO)
bin/parser.opt$(EXE): $(PARSERCMX)