summaryrefslogtreecommitdiff
path: root/man/coqc.1
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-11-21 21:38:49 +0000
commit70b9be8acc1d1ada178a95c1cd4013506e9d0d1b (patch)
treef672a286d962cc67c95874b3b60402fc957870b6 /man/coqc.1
parenta5bd4e097a94cc4f863bf4d4bcc5ce592c30ba47 (diff)
parent208a0f7bfa5249f9795e6e225f309cbe715c0fad (diff)
Merge commit 'upstream/8.1.gamma' into 8.1
Diffstat (limited to 'man/coqc.1')
-rw-r--r--man/coqc.111
1 files changed, 7 insertions, 4 deletions
diff --git a/man/coqc.1 b/man/coqc.1
index 741b3dcb..7113d504 100644
--- a/man/coqc.1
+++ b/man/coqc.1
@@ -32,10 +32,13 @@ For interactive use of Coq, see
.SH OPTIONS
-.TP
-.BI \-h
-Will give you a description of the whole list of options of coqc and
-coqtop.
+.B coqc
+is a script that simply runs
+.B coqtop
+with option
+.B \-compile
+it accepts the same options as
+.B coqtop.
.SH SEE ALSO