diff options
| author | herbelin | 2010-04-09 08:54:04 +0000 |
|---|---|---|
| committer | herbelin | 2010-04-09 08:54:04 +0000 |
| commit | 30488fec6d5c4b78aa3f338be0e6b69f99a4590c (patch) | |
| tree | cf4987f5d0b32e7e97f07425908f67ab5308c3e6 /doc | |
| parent | 69b757baefaddb9d32978d06044c8005f38aa337 (diff) | |
Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing
rules (bug report #2293).
Restored the sequential extension of the printing rules tables (that
commit #12905 replaced by a per-file modification of the printing
rules table). Note however that the table grows in the order of
compilation of files by coqdoc, which does not necessarily coincide
with the order of coqc compilation dependencies of the files.
Added documentation of coqdoc option "--external".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12908 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/coqdoc.tex | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex index 626593fc9d..e00484e6c1 100644 --- a/doc/refman/coqdoc.tex +++ b/doc/refman/coqdoc.tex @@ -386,10 +386,16 @@ Default behavior is to build an index, for the HTML output only, into Do not insert links to the \Coq\ standard library. +\item[\texttt{\mm{}external }\textit{url}~\textit{coqdir}] ~\par + + Use given URL for linking references whose name starts with prefix + \textit{coqdir}. + \item[\texttt{\mm{}coqlib }\textit{url}] ~\par Set base URL for the \Coq\ standard library (default is - \url{http://coq.inria.fr/library/}). + \url{http://coq.inria.fr/library/}). This is equivalent to + \texttt{\mm{}external }\textit{url}~\texttt{Coq}. \item[\texttt{-R }\textit{dir }\textit{coqdir}] ~\par |