aboutsummaryrefslogtreecommitdiffhomepage
path: root/man
diff options
context:
space:
mode:
authorGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-05-02 10:07:25 +0000
committerGravatar notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7>2006-05-02 10:07:25 +0000
commit8de001fbc2dd1a5fcec2bfd9d5fb5f022d4b77be (patch)
tree23564c80be8e3e9e5770278ad516e9572b84ded5 /man
parent140aa7e12c0735b7c3e793436378bf015b5c6dec (diff)
Ajout d'une option --coqlib_path pour Coqdoc (modification suggérée par S. Mimram)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8775 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'man')
-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).