From 30488fec6d5c4b78aa3f338be0e6b69f99a4590c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 9 Apr 2010 08:54:04 +0000
Subject: 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
---
 doc/refman/coqdoc.tex | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'doc')

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
 
-- 
cgit v1.2.3