aboutsummaryrefslogtreecommitdiff
path: root/scripts
diff options
context:
space:
mode:
authorletouzey2007-09-15 10:35:59 +0000
committerletouzey2007-09-15 10:35:59 +0000
commitda3edaa7eab2bed17cdfb2c455f2e6b5b0318c4d (patch)
tree14b6ae25300dc08c9ca5ff86ad88a78910df7b92 /scripts
parent4f39e160d05b0e5501a909b3041589303651670b (diff)
* Adding compability with ocaml 3.10 + camlp5 (rework of
the patch by S. Mimram) * for detecting architecture, also look for /bin/uname * restore the compatibility of kernel/byterun/coq_interp.c with ocaml 3.07 (caml_modify vs. modify). There is still an issue with this 3.07 and 64-bits architecture (see coqdev and a future bug report). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10122 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml7
1 files changed, 5 insertions, 2 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 3654350561..5d35298e8a 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -32,7 +32,10 @@ let ide = split_list Tolink.ide
(* 3. Toplevel objects *)
let camlp4topobjs =
- ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
+ if Coq_config.camlp4 = "camlp5" then
+ ["camlp5_top.cma"; "camlp5o.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
+ else
+ ["camlp4_top.cma"; "pa_o.cmo"; "pa_op.cmo"; "pa_extend.cmo"]
let topobjs = camlp4topobjs
let gramobjs = []
@@ -306,7 +309,7 @@ let main () =
(* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
let args = if !top then args @ [ "topstart.cmo" ] else args in
(* Now, with the .cma, we MUST use the -linkall option *)
- let command = String.concat " " (prog::args) in
+ let command = String.concat " " (prog::"-rectypes"::args) in
if !echo then
begin
print_endline command;