aboutsummaryrefslogtreecommitdiffhomepage
path: root/man/coqdoc.1
diff options
context:
space:
mode:
Diffstat (limited to 'man/coqdoc.1')
-rw-r--r--man/coqdoc.14
1 files changed, 4 insertions, 0 deletions
diff --git a/man/coqdoc.1 b/man/coqdoc.1
index 1d294c742..c443e8b04 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -125,6 +125,10 @@ Do not insert links to the Coq standard library.
Set base URL for the Coq standard library (default is http://coq.inria.fr/library/).
.TP
+.BI \-\-coqlib_path \ dir
+Set the base path where the Coq files are installed, especially style files coqdoc.sty and coqdoc.css.
+
+.TP
.BI -R \ dir \ coqdir
Map physical directory dir to Coq logical directory coqdir (similarly
to Coq option -R).