aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/envars.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-28 21:02:48 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-12-10 18:41:16 +0100
commit598e3ae4a8eb8d9bce316e13d71ee48d9ba1a01f (patch)
tree7bf3135dea14dfccac59a6b373549b6bddec7741 /lib/envars.ml
parentd0f89f8c59cda2e7e74fec693e511e910fbc0434 (diff)
[build] Remove coqmktop in favor of ocamlfind.
We remove coqmktop in favor of a couple of simple makefile rules using ocamlfind. In order to do that, we introduce a new top-level file that calls the coqtop main entry. This is very convenient in order to use other builds systems such as `ocamlbuild` or `jbuilder`. An additional consideration is that we must perform a side-effect on init depending on whether we have an OCaml toplevel available [byte] or not. We do that by using two different object files, one for the bytecode version other for the native one, but we may want to review our choice. We also perform some smaller cleanups taking profit from ocamlfind.
Diffstat (limited to 'lib/envars.ml')
-rw-r--r--lib/envars.ml12
1 files changed, 5 insertions, 7 deletions
diff --git a/lib/envars.ml b/lib/envars.ml
index 206d75033..8ebf84057 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -153,19 +153,17 @@ let coqpath =
let exe s = s ^ Coq_config.exec_extension
-let ocamlfind () =
- if !Flags.ocamlfind_spec then !Flags.ocamlfind else Coq_config.ocamlfind
+let ocamlfind () = Coq_config.ocamlfind
(** {2 Camlp4 paths} *)
let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4)
let camlp4bin () =
- if !Flags.camlp4bin_spec then !Flags.camlp4bin else
- if !Flags.boot then Coq_config.camlp4bin else
- try guess_camlp4bin ()
- with Not_found ->
- Coq_config.camlp4bin
+ if !Flags.boot then Coq_config.camlp4bin else
+ try guess_camlp4bin ()
+ with Not_found ->
+ Coq_config.camlp4bin
let camlp4 () = camlp4bin () / exe Coq_config.camlp4