aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/practical-tools/utilities.rst
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/practical-tools/utilities.rst')
-rw-r--r--doc/sphinx/practical-tools/utilities.rst4
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst
index 408f8fc3ec..33ebbce640 100644
--- a/doc/sphinx/practical-tools/utilities.rst
+++ b/doc/sphinx/practical-tools/utilities.rst
@@ -170,6 +170,10 @@ Here we describe only few of them.
override the flags passed to ``coqdoc``. By default ``-interpolate -utf8``.
:COQDOCEXTRAFLAGS:
extend the flags passed to ``coqdoc``
+:COQLIBINSTALL, COQDOCINSTALL:
+ specify where the Coq libraries and documentation will be installed.
+ By default a combination of ``$(DESTDIR)`` (if defined) with
+ ``$(COQLIB)/user-contrib`` and ``$(DOCDIR)/user-contrib``.
**Rule extension**