diff options
| author |  pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-21 16:58:23 +0000 |
|---|---|---|
| committer | pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-21 16:58:23 +0000 |
| commit | 885bddb65bd236d2e1e9e8c5a44cec688036213b (patch) | |
| tree | 0916fe71c291d8a46138681a7d1a6fc5c83d51ca /doc | |
| parent | 36404268502d43a657c1cdc4bcb7bbdc972b6c56 (diff) | |
/home/pirbo/.coqrc* are read again
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14714 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 0f4bb342a..81d94ecf0 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -57,7 +57,7 @@ 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 +\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:). |