diff options
Diffstat (limited to 'doc/refman')
| -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:). |