diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-26 15:00:33 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-09-26 15:20:43 +0200 |
commit | 5481ff4f6935874ac3798a61f5a2a810006bde37 (patch) | |
tree | 07394b2faa06520edde9c288a8ea946fbd9257f6 /tools | |
parent | 802f3a5c313c8ef98109a3f29c3c862de63bd53c (diff) |
Clarifying the doc of coqdoc --utf8 as discussed on coq-club on August 19, 2015.
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coqdoc/main.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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"; |