aboutsummaryrefslogtreecommitdiff
path: root/man/coqide.1
diff options
context:
space:
mode:
authorThéo Zimmermann2020-04-02 15:51:09 +0200
committerThéo Zimmermann2020-04-02 22:14:01 +0200
commit0c1382bd0a9c41b559a912695e2154b758de7b18 (patch)
tree6a2749527fd05e837bceb3e5435be0328572e116 /man/coqide.1
parentefa833d06990262174195fdc43a542d272b480a3 (diff)
Minimal fix to man pages.
Diffstat (limited to 'man/coqide.1')
-rw-r--r--man/coqide.12
1 files changed, 1 insertions, 1 deletions
diff --git a/man/coqide.1 b/man/coqide.1
index 62a102af03..c1af046019 100644
--- a/man/coqide.1
+++ b/man/coqide.1
@@ -69,7 +69,7 @@ Load Coq library
(Require
.IR path .).
.TP
-.BI \-require\ path
+.BI \-require-import\ path
Load Coq library
.IR path
and import it (Require Import