aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-com.tex
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-20 20:02:54 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-11-20 20:02:54 +0000
commit1c535a5a1e6f4dcc35bd67a99a7236c6e7a222ab (patch)
tree7803c5a9ed6bb9327d24ac0920e4f3e96b111a04 /doc/refman/RefMan-com.tex
parent665652844458aa9826e425864781860504bf1836 (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/refman/RefMan-com.tex')
-rw-r--r--doc/refman/RefMan-com.tex5
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex
index 5af57aefc..17efcb7b5 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}}