aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--doc/refman/RefMan-com.tex15
-rw-r--r--lib/envars.ml5
-rw-r--r--lib/envars.mli1
-rw-r--r--lib/system.ml2
-rw-r--r--toplevel/coqinit.ml8
5 files changed, 19 insertions, 12 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 17efcb7b5..076519dc6 100644
--- a/doc/refman/RefMan-com.tex
+++ b/doc/refman/RefMan-com.tex
@@ -53,13 +53,14 @@ native-code versions of the system.
\section[Resource file]{Resource file\index{Resource file}}
When \Coq\ is launched, with either {\tt coqtop} or {\tt coqc}, the
-resource file \verb:$HOME/.coqrc.xxx: is loaded, where \verb:$HOME: is
-the home directory of the user and \verb:xxx: is the version number
-(e.g. 8.3). If this file is not found, then the file
-\verb:$HOME/.coqrc: is searched. You can also specify an arbitrary
-name for the resource file (see option \verb:-init-file: below), or
-the name of another user to load the resource file of someone else
-(see option \verb:-user:).
+resource file \verb:$XDG_CONFIG_HOME/coq/coqrc.xxx: is loaded, where
+\verb:$XDG_CONFIG_HOME: is the configuration directory of the user (by
+default its home directory \verb!/.config! and \verb:xxx: is the version
+number (e.g. 8.3). If this file is not found, then the file
+\verb:$XDG_CONFIG_HOME/.coqrc: is searched. You can also specify an
+arbitrary name for the resource file (see option \verb:-init-file:
+below), or the name of another user to load the resource file of someone
+else (see option \verb:-user:).
This file may contain, for instance, \verb:Add LoadPath: commands to add
diff --git a/lib/envars.ml b/lib/envars.ml
index 5cffad06c..dc71cb433 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -56,6 +56,11 @@ let xdg_data_home =
(System.getenv_else "XDG_DATA_HOME" (Filename.concat System.home ".local/share"))
"coq"
+let xdg_config_home =
+ Filename.concat
+ (System.getenv_else "XDG_CONFIG_HOME" (Filename.concat System.home ".config"))
+ "coq"
+
let xdg_data_dirs =
try
List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
diff --git a/lib/envars.mli b/lib/envars.mli
index d2799074e..0c80492f8 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -15,6 +15,7 @@ val coqbin : string
val coqroot : string
(* coqpath is stored in reverse order, since that is the order it
* gets added to the searc path *)
+val xdg_config_home : string
val xdg_dirs : string list
val coqpath : string list
diff --git a/lib/system.ml b/lib/system.ml
index edab24460..7d54e2c3a 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -33,7 +33,7 @@ let home =
try Sys.getenv "USERPROFILE" with Not_found ->
warning ("Cannot determine user home directory, using '.' .");
flush_all ();
- "."
+ Filename.current_dir_name
let safe_getenv n = safe_getenv_def n ("$"^n)
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 0c6286d3a..7d178ede3 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -15,13 +15,13 @@ let (/) = Filename.concat
let set_debug () = Flags.debug := true
(* Loading of the ressource file.
- rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one
+ rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one
does not exist. *)
-let rcfile = ref (home/".coqrc")
+let rcfile = ref (Envars.xdg_config_home/"coqrc")
let rcfile_specified = ref false
let set_rcfile s = rcfile := s; rcfile_specified := true
-let set_rcuser s = rcfile := ("~"^s)/".coqrc"
+let set_rcuser s = rcfile := ("~"^s)^"/.config/coq/coqrc"
let load_rc = ref true
let no_load_rc () = load_rc := false
@@ -40,7 +40,7 @@ let load_rcfile() =
else ()
(*
Flags.if_verbose
- mSGNL (str ("No .coqrc or .coqrc."^Coq_config.version^
+ mSGNL (str ("No coqrc or coqrc."^Coq_config.version^
" found. Skipping rcfile loading."))
*)
with e ->