summaryrefslogtreecommitdiff
path: root/man
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /man
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'man')
-rw-r--r--man/coqdoc.113
1 files changed, 10 insertions, 3 deletions
diff --git a/man/coqdoc.1 b/man/coqdoc.1
index 4a2fddee..c443e8b0 100644
--- a/man/coqdoc.1
+++ b/man/coqdoc.1
@@ -1,4 +1,4 @@
-.TH coqdoc 1 "December, 2005"
+.TH coqdoc 1 "April, 2006"
.SH NAME
coqdoc \- A documentation tool for the Coq proof assistant
@@ -43,6 +43,9 @@ Select a PostScript output.
.B \-\-texmacs
Select a TeXmacs output.
.TP
+.B \-\-stdout
+Redirect the output to stdout
+.TP
.BI \-o \ file, \-\-output \ file
Redirect the output into the file
.I file.
@@ -81,7 +84,7 @@ Be quiet. Do not print anything except errors.
.B \-h, \ \-\-help
Give a short summary of the options and exit.
.TP
-.BI
+.B
\-v, \ \-\-version
Print the version and exit.
@@ -122,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).
@@ -168,7 +175,7 @@ http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.
Give a LATEX input encoding, as an option to LATEX package inputenc.
.TP
-.BI --charset string
+.BI --charset \ string
Specify the HTML character set, to be inserted in the HTML header.