refman/coqdoc.tex: fix two erroneous \url

coq · Dec 9, 2014 · a9457a0 · a9457a0
1 parent 6d0f9aa
commit a9457a0
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
@@ -197,8 +197,8 @@ \subsection{Principles}
 
 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.}