aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/envars.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-12 23:59:52 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-03-12 23:59:52 +0000
commit027618d5aa99613ffbe390371cda492690809cc7 (patch)
tree173636aff2f8e73d3b3da93362c0b94945650100 /lib/envars.ml
parentd5c15e8836c2225fceaf7f2abc564b04dec653ee (diff)
Restrict (try...with...) to avoid catching critical exn (part 4)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16280 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/envars.ml')
-rw-r--r--lib/envars.ml18
1 files changed, 8 insertions, 10 deletions
diff --git a/lib/envars.ml b/lib/envars.ml
index 47ecdb400..84a41f8e4 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -154,7 +154,7 @@ let guess_camlbin () = which (user_path ()) (exe "ocamlc")
let camlbin () =
if !Flags.camlbin_spec then !Flags.camlbin else
if !Flags.boot then Coq_config.camlbin else
- try guess_camlbin () with _ -> Coq_config.camlbin
+ try guess_camlbin () with Not_found -> Coq_config.camlbin
let ocamlc () = camlbin () / Coq_config.ocamlc
@@ -175,15 +175,13 @@ 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 _ ->
- if Sys.file_exists (camlbin () / exe Coq_config.camlp4) then
- camlbin ()
- else
- Coq_config.camlp4bin
-
-let camlp4 () = camlp4bin () / Coq_config.camlp4
+ try guess_camlp4bin ()
+ with Not_found ->
+ let cb = camlbin () in
+ if Sys.file_exists (cb / exe Coq_config.camlp4) then cb
+ else Coq_config.camlp4bin
+
+let camlp4 () = camlp4bin () / exe Coq_config.camlp4
let camlp4lib () =
if !Flags.boot then