diff options
Diffstat (limited to 'man/coqdoc.1')
| -rw-r--r-- | man/coqdoc.1 | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/man/coqdoc.1 b/man/coqdoc.1 index e07ccdd3..8d71a874 100644 --- a/man/coqdoc.1 +++ b/man/coqdoc.1 @@ -121,6 +121,10 @@ globalizations are obtained with Coq option \-dump\-glob). Do not insert links to the Coq standard library. .TP +.BI \-\-external \ url \ libroot +Set base URL for the external library whose root prefix is libroot. + +.TP .BI \-\-coqlib \ url Set base URL for the Coq standard library (default is http://coq.inria.fr/library/). |