diff options
| author | pboutill | 2011-04-08 16:26:16 +0000 |
|---|---|---|
| committer | pboutill | 2011-04-08 16:26:16 +0000 |
| commit | c229186019d23d9893a12c5aae9a0f128f013a3d (patch) | |
| tree | 8cfc3f353ec8abe521da9c29328194da307b2674 | |
| parent | 27aa815d451fc21469019137399287196d9a187b (diff) | |
A kind of reply to bug 2444
coq_makefile uses ocaml{c,opt}.opt if it uses coqc -opt and ocamlâc,opt}
if it uses coqc -byte.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13980 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tools/coq_makefile.ml4 | 23 |
1 files changed, 13 insertions, 10 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index a08506883a..55bd2f5602 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -40,11 +40,6 @@ let rec print_list sep = function let list_iter_i f = let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1 -let best_ocamlc = - if Coq_config.best = "opt" then "ocamlc.opt" else "ocamlc" -let best_ocamlopt = - if Coq_config.best = "opt" then "ocamlopt.opt" else "ocamlopt" - let section s = let l = String.length s in let sep = String.make (l+5) '#' @@ -279,11 +274,19 @@ let variables defs = print "COQDOC:=$(COQBIN)coqdoc\n"; print "COQMKTOP:=$(COQBIN)coqmktop\n"; (* Caml executables and relative variables *) - printf "CAMLLIB:=$(shell $(CAMLBIN)%s -where)\n" best_ocamlc; - printf "CAMLC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlc; - printf "CAMLOPTC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlopt; - printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; - printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; + print "CAMLLIB:=$(shell $(CAMLBIN)ocamlc -where)\n"; + let pp_ocamlc s = + printf "CAMLC:=$(CAMLBIN)ocamlc%s -c -rectypes\n" s; + printf "CAMLOPTC:=$(CAMLBIN)ocamlopt%s -c -rectypes\n" s; + printf "CAMLLINK:=$(CAMLBIN)ocamlc%s -rectypes\n" s; + printf "CAMLOPTLINK:=$(CAMLBIN)ocamlopt%s -rectypes\n" s; + in if !opt = "-opt" then begin + print "ifeq ($(OPT),-byte)\n"; + pp_ocamlc ""; + print "else\n"; + pp_ocamlc ".opt"; + print "endif\n"; + end else pp_ocamlc ""; print "GRAMMARS:=grammar.cma\n"; print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; print "CAMLP4OPTIONS:=\n"; |