diff options
| author | pboutill | 2011-11-20 20:02:54 +0000 |
|---|---|---|
| committer | pboutill | 2011-11-20 20:02:54 +0000 |
| commit | 1c535a5a1e6f4dcc35bd67a99a7236c6e7a222ab (patch) | |
| tree | 7803c5a9ed6bb9327d24ac0920e4f3e96b111a04 /doc | |
| parent | 665652844458aa9826e425864781860504bf1836 (diff) | |
Add support for XDG_DATA_HOME and XDG_DATA_DIRS.
From Tom Prince
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14692 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-com.tex | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 5af57aefc5..17efcb7b5f 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -82,6 +82,11 @@ only for developers that are writing their own tactics and are using (defined at installation time). So these variables are useful only if you move the \Coq\ binaries and library after installation. +Coq will also honor \verb:$XDG_DATA_HOME: and \verb:$XDG_DATA_DIRS: (see +\{http://standards.freedesktop.org/basedir-spec/basedir-spec-latest.html}). +Coq adds \verb:${XDG_DATA_HOME}/coq: and \verb:${XDG_DATA_DIRS}/coq: to its +search path. + \section[Options]{Options\index{Options of the command line} \label{vmoption} \label{coqoptions}} |