diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:52 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-12 23:59:52 +0000 |
commit | 027618d5aa99613ffbe390371cda492690809cc7 (patch) | |
tree | 173636aff2f8e73d3b3da93362c0b94945650100 /lib/envars.ml | |
parent | d5c15e8836c2225fceaf7f2abc564b04dec653ee (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.ml | 18 |
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 |