aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-09-26 15:00:33 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-09-26 15:20:43 +0200
commit5481ff4f6935874ac3798a61f5a2a810006bde37 (patch)
tree07394b2faa06520edde9c288a8ea946fbd9257f6
parent802f3a5c313c8ef98109a3f29c3c862de63bd53c (diff)
Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.
-rw-r--r--doc/refman/coqdoc.tex14
-rw-r--r--tools/coqdoc/main.ml4
2 files changed, 10 insertions, 8 deletions
diff --git a/doc/refman/coqdoc.tex b/doc/refman/coqdoc.tex
index ee2b042f4..30467a5e6 100644
--- a/doc/refman/coqdoc.tex
+++ b/doc/refman/coqdoc.tex
@@ -285,7 +285,7 @@ suffix \verb!.tex!.
Select a \texmacs\ output.
-\item[\texttt{--stdout}] ~\par
+\item[\texttt{\mm{}stdout}] ~\par
Write output to stdout.
@@ -496,14 +496,16 @@ Default behavior is to assume ASCII 7 bits input files.
\item[\texttt{-latin1}, \texttt{\mm{}latin1}] ~\par
Select ISO-8859-1 input files. It is equivalent to
- \texttt{--inputenc latin1 --charset iso-8859-1}.
+ \texttt{\mm{}inputenc latin1 \mm{}charset iso-8859-1}.
\item[\texttt{-utf8}, \texttt{\mm{}utf8}] ~\par
- Select UTF-8 (Unicode) input files. It is equivalent to
- \texttt{--inputenc utf8 --charset utf-8}.
- \LaTeX\ UTF-8 support can be found at
- \url{http://www.ctan.org/pkg/unicode}.
+ Set \texttt{\mm{}inputenc utf8x} for \LaTeX\ output and
+ \texttt{\mm{}charset utf-8} for HTML output. Also use Unicode
+ replacements for a couple of standard plain ASCII notations such
+ as $\rightarrow$ for \texttt{->} and $\forall$ for
+ \texttt{forall}. \LaTeX\ UTF-8 support can be found at
+ \url{http://www.ctan.org/pkg/unicode}.
\item[\texttt{\mm{}inputenc} \textit{string}] ~\par
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 2554ed495..22febd6a6 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -61,8 +61,8 @@ let usage () =
prerr_endline " --coqlib_path <dir> set the path where Coq files are installed";
prerr_endline " -R <dir> <coqdir> map physical dir to Coq dir";
prerr_endline " -Q <dir> <coqdir> map physical dir to Coq dir";
- prerr_endline " --latin1 set ISO-8859-1 input language";
- prerr_endline " --utf8 set UTF-8 input language";
+ prerr_endline " --latin1 set ISO-8859-1 mode";
+ prerr_endline " --utf8 set UTF-8 mode";
prerr_endline " --charset <string> set HTML charset";
prerr_endline " --inputenc <string> set LaTeX input encoding";
prerr_endline " --interpolate try to typeset identifiers in comments using definitions in the same module";