aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-12-14 17:17:29 +0100
committerPierre-Marie Pédrot2020-12-14 17:17:29 +0100
commit8fc64949349a003d28e8a7341e3038a1ed993128 (patch)
tree2aedecd4324d7803f51f9c2a2753992da9a2ed49 /lib
parentd5ca91cc6989759f0a467644a47979413f2c1f47 (diff)
parent9fb840fa5f33f593bc204765a13c027155559c2e (diff)
Merge PR #13523: [envars] honor file "coq_environment.txt"
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48 Ack-by: ejgallego Ack-by: herbelin Ack-by: ppedrot
Diffstat (limited to 'lib')
-rw-r--r--lib/envars.ml34
1 files changed, 32 insertions, 2 deletions
diff --git a/lib/envars.ml b/lib/envars.ml
index 585d5185b4..1702b5d7a2 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -12,7 +12,37 @@ open Util
(** {1 Helper functions} *)
-let getenv_else s dft = try Sys.getenv s with Not_found -> dft ()
+let parse_env_line l =
+ try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
+ with _ -> None
+
+let with_ic file f =
+ let ic = open_in file in
+ try
+ let rc = f ic in
+ close_in ic;
+ rc
+ with e -> close_in ic; raise e
+
+let getenv_from_file name =
+ let base = Filename.dirname Sys.executable_name in
+ try
+ with_ic (base ^ "/coq_environment.txt") (fun ic ->
+ let rec find () =
+ let l = input_line ic in
+ match parse_env_line l with
+ | Some(n,v) when n = name -> v
+ | _ -> find ()
+ in
+ find ())
+ with
+ | Sys_error s -> raise Not_found
+ | End_of_file -> raise Not_found
+
+let system_getenv name =
+ try Sys.getenv name with Not_found -> getenv_from_file name
+
+let getenv_else s dft = try system_getenv s with Not_found -> dft ()
let safe_getenv warning n =
getenv_else n (fun () ->
@@ -145,7 +175,7 @@ let coqpath =
(** {2 Caml paths} *)
-let ocamlfind () = Coq_config.ocamlfind
+let ocamlfind () = getenv_else "OCAMLFIND" (fun () -> Coq_config.ocamlfind)
(** {1 XDG utilities} *)