aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/system.ml2
-rw-r--r--lib/system.mli2
2 files changed, 3 insertions, 1 deletions
diff --git a/lib/system.ml b/lib/system.ml
index 7e59a876e0..d14956daf9 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -22,6 +22,8 @@ let safe_getenv_def var def =
flush Pervasives.stdout;
def
+let getenv_else s dft = try Sys.getenv s with Not_found -> dft
+
let home = (safe_getenv_def "HOME" ".")
let safe_getenv n = safe_getenv_def n ("$"^n)
diff --git a/lib/system.mli b/lib/system.mli
index 1ecd4bcffa..279a6dc3e5 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -24,7 +24,7 @@ val make_suffix : string -> string -> string
val file_readable_p : string -> bool
val glob : string -> string
-
+val getenv_else : string -> string -> string
val home : string
val exists_dir : string -> bool