diff options
author | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-20 20:03:06 +0000 |
---|---|---|
committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-20 20:03:06 +0000 |
commit | 5ec2163ce648db25aba87f5208841397fd2e1b1c (patch) | |
tree | 7605292fdb65b235b98f315cc07694363c286ba5 /doc/refman | |
parent | ab6f28a2a5251cc7ef18948dc619781e82e43e71 (diff) |
coqrc in the right XDG_CONFIG_HOME/coq folder
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14696 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/RefMan-com.tex | 15 |
1 files changed, 8 insertions, 7 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 |