aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorThéo Zimmermann2017-05-20 10:28:17 +0200
committerThéo Zimmermann2017-05-20 10:28:17 +0200
commitaae960fc0ed0a3a8d244c1c3d7c5363c17044cbc (patch)
tree0687c0311c15bd7be199ea674945883d4c6f25bd
parent9f11adda4bff194a3c6a66d573ce7001d4399886 (diff)
Mention ./configure in INSTALL.doc
As prompted in https://coq.inria.fr/bugs/show_bug.cgi?id=2831
-rw-r--r--INSTALL.doc5
1 files changed, 5 insertions, 0 deletions
diff --git a/INSTALL.doc b/INSTALL.doc
index 2472d2b2a6..21b21163c0 100644
--- a/INSTALL.doc
+++ b/INSTALL.doc
@@ -41,6 +41,7 @@ Compilation
To produce all documentation about Coq, just run:
+ ./configure (if you hadn't already)
make doc
@@ -71,6 +72,10 @@ Alternatively, you can use some specific targets:
to produce all formats of the Coq standard library
+Also note the "-with-doc yes" option of ./configure to enable the
+build of the documentation as part of the default make target.
+
+
Installation
------------