aboutsummaryrefslogtreecommitdiffhomepage
path: root/scripts
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-12 07:41:13 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-07-12 07:41:13 +0000
commiteabacd04872bda164e222cdc9b48a1ee95631c8a (patch)
treef8cb18e46b485af966bea5501a0ba347aa8f1c87 /scripts
parentb579b8930f4fa70d50d1934a9a96871d2e8d9fae (diff)
Coq should compile with Ocaml4 and/or lablgtk installed with ocamlfind
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15603 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'scripts')
-rw-r--r--scripts/coqmktop.ml9
1 files changed, 7 insertions, 2 deletions
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 55e12a30e..bd4dec2b6 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -52,6 +52,8 @@ let top = ref false
let echo = ref false
let no_start = ref false
+let is_ocaml4 = String.sub Coq_config.caml_version 0 2 = "4."
+
let src_dirs () =
[ []; ["kernel";"byterun"]; [ "config" ]; [ "toplevel" ] ]
@@ -62,7 +64,8 @@ let includes () =
(fun d l -> "-I" :: ("\"" ^ List.fold_left Filename.concat coqlib d ^ "\"") :: l)
(src_dirs ())
(["-I"; "\"" ^ camlp4lib ^ "\""] @
- ["-I"; "\"" ^ coqlib ^ "\""])
+ ["-I"; "\"" ^ coqlib ^ "\""] @
+ if is_ocaml4 then ["-I"; "+compiler-libs"] else [])
(* Transform bytecode object file names in native object file names *)
let native_suffix f =
@@ -261,7 +264,9 @@ let main () =
ocamloptexec^" -linkall"
end else
(* bytecode (we shunt ocamlmktop script which fails on win32) *)
- let ocamlmktoplib = " toplevellib.cma" in
+ let ocamlmktoplib = if is_ocaml4
+ then " ocamlcommon.cma ocamlbytecomp.cma ocamltoplevel.cma"
+ else " toplevellib.cma" in
let ocamlcexec = Filename.concat camlbin "ocamlc" in
let ocamlccustom = Printf.sprintf "%s %s -linkall "
ocamlcexec Coq_config.coqrunbyteflags in