diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-12 13:53:10 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-05-16 12:36:47 +0200 |
commit | 0a8d0181d4f9ae7440b0daf065511342cef41475 (patch) | |
tree | f1e86770a24ba76da05d2a8b1bc8116d48c58173 /doc | |
parent | 12109393c957ef64f7dc8d47b745a75392e4382c (diff) |
Minor update of the documentation/man about the resource file.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 83dddab4f..ad1f0caa6 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -55,15 +55,20 @@ Customization at launch time By resource file ~~~~~~~~~~~~~~~~~~~~~~~ -When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file -``$XDG_CONFIG_HOME/coq/coqrc.xxx`` is loaded, where ``$XDG_CONFIG_HOME`` +When |Coq| is launched, with either ``coqtop`` or ``coqc``, the +resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will +be implicitly prepended to any document read by Coq, whether it is an +interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME`` is the configuration directory of the user (by default its home -directory ``/.config`` and ``xxx`` is the version number (e.g. 8.8). If +directory ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is -searched. You can also specify an arbitrary name for the resource file +searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched, +and, if still not found, the file ``~/.coqrc``. If the latter is also +absent, no resource file is loaded. +You can also specify an arbitrary name for the resource file (see option ``-init-file`` below). -This file may contain, for instance, ``Add LoadPath`` commands to add +The resource file may contain, for instance, ``Add LoadPath`` commands to add directories to the load path of |Coq|. It is possible to skip the loading of the resource file with the option ``-q``. |