aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/envars.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-11-11 11:11:20 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-05-29 11:21:21 +0200
commit417ac448411ce924444915da8e7e6fb81a12bc57 (patch)
treef9ab75068617f0c0a598e058da206803883d0103 /lib/envars.ml
parent168bb8fd5fe62beebd5e4998e903777b33654a4a (diff)
Configuration: always giving a value to configdir and datadir.
They were not used for looking for coqide files in the situation when the effective installation path happens to be exactly the installation path proposed by default, while relevant files were however (possibly) installed in these directories.
Diffstat (limited to 'lib/envars.ml')
-rw-r--r--lib/envars.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/lib/envars.ml b/lib/envars.ml
index 0974368f6..989a18db9 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -23,8 +23,6 @@ let ( / ) a b =
let coqify d = d / "coq"
-let opt2list = function None -> [] | Some x -> [x]
-
let home ~warn =
getenv_else "HOME" (fun () ->
try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
@@ -189,7 +187,7 @@ let xdg_data_dirs warn =
| Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "share"]
| Not_found -> ["/usr/local/share/coq";"/usr/share/coq"]
in
- xdg_data_home warn :: sys_dirs @ opt2list Coq_config.datadir
+ xdg_data_home warn :: sys_dirs @ [Coq_config.datadir]
let xdg_dirs ~warn =
List.filter Sys.file_exists (xdg_data_dirs warn)