aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
authorEnrico Tassi2020-11-30 15:06:21 +0100
committerEnrico Tassi2020-12-04 11:58:00 +0100
commit823a5a0ca12e574fa4d9851f76b28d0a78baa118 (patch)
tree96a04cf89547906fd1c3600406b3a81ed24c0dcd /lib
parent1b39124d33f609740bb601ee5468f39470ba540b (diff)
[win] [envars] honor file "coq_environment.txt"
On windows we provide a way to set environment variables local to a coq installation by providing a file named "coq_environment.txt" containing KEY="value" pairs. No space between KEY and = is allowed, values are in quotes according to OCaml's escaping conventions. The file is line-directed, illformed lines are skipped.
Diffstat (limited to 'lib')
-rw-r--r--lib/envars.ml32
1 files changed, 31 insertions, 1 deletions
diff --git a/lib/envars.ml b/lib/envars.ml
index 0455e8305b..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 () ->