diff options
| author | Pierre Letouzey | 2014-01-30 15:49:15 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-01-30 18:36:50 +0100 |
| commit | 2fa5d8befba9ef24629233a3620494760583f75f (patch) | |
| tree | f7435fbe5f29a49734796b3e336013e3f53d208c /lib/envars.ml | |
| parent | 84b09aae2c727877c98e02508ddcd3b6a3ee9db7 (diff) | |
CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleaned
Diffstat (limited to 'lib/envars.ml')
| -rw-r--r-- | lib/envars.ml | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/lib/envars.ml b/lib/envars.ml index 5e20df3585..0247058218 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -155,11 +155,10 @@ let ocamlc () = camlbin () / Coq_config.ocamlc let ocamlopt () = camlbin () / Coq_config.ocamlopt let camllib () = - if !Flags.boot then + if !Flags.boot then Coq_config.camllib else - let com = ocamlc () ^ " -where" in - let _, res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in + let _, res = CUnix.run_command (ocamlc () ^ " -where") in String.strip res (** {2 Camlp4 paths} *) @@ -181,8 +180,7 @@ let camlp4lib () = if !Flags.boot then Coq_config.camlp4lib else - let com = camlp4 () ^ " -where" in - let ex, res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in + let ex, res = CUnix.run_command (camlp4 () ^ " -where") in match ex with | Unix.WEXITED 0 -> String.strip res | _ -> "/dev/null" |