aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 15:23:08 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-12-07 15:23:08 +0000
commitce359ab8e44ad3df5b6f9eb27125e405b987f068 (patch)
tree62a0299a4da4a207513e1e7d1b7eae6f1d8b86b8 /lib
parentf3ef0567258237d80fd3f8722b50604dec5de02c (diff)
Envars: repair failed compilation after yann's commits
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16040 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib')
-rw-r--r--lib/envars.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/lib/envars.ml b/lib/envars.ml
index b8111831b..b6312e7d9 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -151,6 +151,10 @@ let camlbin () =
if !Flags.boot then Coq_config.camlbin else
try guess_camlbin () with _ -> Coq_config.camlbin
+let ocamlc () = camlbin () / Coq_config.ocamlc
+
+let ocamlopt () = camlbin () / Coq_config.ocamlopt
+
let camllib () =
if !Flags.boot then
Coq_config.camllib
@@ -159,10 +163,6 @@ let camllib () =
let _, res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in
Util.String.strip res
-let ocamlc () = camlbin () / Coq_config.ocamlc
-
-let ocamlopt () = camlbin () / Coq_config.ocamlopt
-
(** {2 Camlp4 paths} *)
let guess_camlp4bin () = which (user_path ()) Coq_config.camlp4