aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/checker.ml
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-20 20:02:54 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-20 20:02:54 +0000
commit1c535a5a1e6f4dcc35bd67a99a7236c6e7a222ab (patch)
tree7803c5a9ed6bb9327d24ac0920e4f3e96b111a04 /checker/checker.ml
parent665652844458aa9826e425864781860504bf1836 (diff)
Add support for XDG_DATA_HOME and XDG_DATA_DIRS.
From Tom Prince git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'checker/checker.ml')
-rw-r--r--checker/checker.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index 098b89469..34ba7b010 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -102,7 +102,8 @@ let set_rec_include d p =
let init_load_path () =
let coqlib = Envars.coqlib () in
let user_contrib = coqlib/"user-contrib" in
- let coqpath = Envars.coqpath () in
+ let xdg_dirs = Envars.xdg_dirs in
+ let coqpath = Envars.coqpath in
let plugins = coqlib/"plugins" in
(* NOTE: These directories are searched from last to first *)
(* first standard library *)
@@ -112,6 +113,8 @@ let init_load_path () =
(* then user-contrib *)
if Sys.file_exists user_contrib then
add_rec_path ~unix_path:user_contrib ~coq_root:Check.default_root_prefix;
+ (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME *)
+ List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) xdg_dirs;
(* then directories in COQPATH *)
List.iter (fun s -> add_rec_path ~unix_path:s ~coq_root:Check.default_root_prefix) coqpath;
(* then current directory *)