diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-11-11 11:11:20 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-29 11:21:21 +0200 |
commit | 417ac448411ce924444915da8e7e6fb81a12bc57 (patch) | |
tree | f9ab75068617f0c0a598e058da206803883d0103 /lib/envars.ml | |
parent | 168bb8fd5fe62beebd5e4998e903777b33654a4a (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.ml | 4 |
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) |