From ff76518771d1da2a7d3c1b1cbb8d637d2f4d7bf7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Tue, 9 Dec 2014 09:26:39 +0100
Subject: refman/coqdoc.tex: fix two erroneous \url

---
 doc/refman/coqdoc.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index c2591a7b9b..fddee4560d 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -197,8 +197,8 @@ Then invoke \texttt{coqdoc} or \texttt{coqdoc \mm{}glob-from \emph{file}} to tel
 
 Identifiers from the \Coq\ standard library are linked to the \Coq\
 web site at \url{http://coq.inria.fr/library/}. This behavior can be
-changed using command line options \url{--no-externals} and
-\url{--coqlib}; see below.
+changed using command line options \texttt{\mm{}no-externals} and
+\texttt{\mm{}coqlib}; see below.
 
 
 \paragraph{Hiding / Showing parts of the source.}
-- 
cgit v1.2.3