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 | |
| parent | 12109393c957ef64f7dc8d47b745a75392e4382c (diff) | |
Minor update of the documentation/man about the resource file.
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 15 | ||||
| -rw-r--r-- | man/coqtop.1 | 2 |
2 files changed, 11 insertions, 6 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``. diff --git a/man/coqtop.1 b/man/coqtop.1 index b1fbb3262..084adfe45 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -110,7 +110,7 @@ print Coq version and exit .TP .B \-q -skip loading of rcfile +skip loading of rcfile (resource file) if any .TP .BI \-init\-file \ filename |