aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authornotin2007-12-18 17:17:16 +0000
committernotin2007-12-18 17:17:16 +0000
commit817f27007e3ff6f537c80b0496c0379191c391d4 (patch)
treed0de7fb5a421a1e5b4e4309186316d5ad8dd3cb7
parent4e46910029be4738d2002d701cda99986b87e610 (diff)
Petite correction sur coq_makefile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10391 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--tools/coq_makefile.ml46
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 478040ddb1..3c92a904ba 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -176,8 +176,8 @@ let variables l =
| _ :: r -> var_aux r
in
section "Variables definitions.";
- print "CAMLP4LIB=`camlp5 -where 2> /dev/null || camlp4 -where`\n";
- print "CAMLP4=`basename $CAMLP4LIB`\n";
+ print "CAMLP4LIB=$(shell camlp5 -where 2> /dev/null || camlp4 -where)\n";
+ print "CAMLP4=$(notdir $(CAMLP4LIB))\n";
(* print "MAKE=make \"COQBIN=$(COQBIN)\" \"OPT=$(OPT)\"\n"; *)
print "COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
-I $(COQTOP)/library -I $(COQTOP)/parsing \\
@@ -200,7 +200,7 @@ let variables l =
print "COQC=$(COQBIN)coqc\n";
print "GALLINA=$(COQBIN)gallina\n";
print "COQDOC=$(COQBIN)coqdoc\n";
- print "CAMLC=ocamlc -c\n";
+ print "CAMLC=ocamlc -rectypes -c\n";
print "CAMLOPTC=ocamlopt -c\n";
print "CAMLLINK=ocamlc\n";
print "CAMLOPTLINK=ocamlopt\n";