summaryrefslogtreecommitdiff
path: root/tools/coqdoc/output.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-11-13 11:31:34 +0100
commit2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch)
tree074182834cb406d1304aec4233718564a9c06ba1 /tools/coqdoc/output.ml
parent0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff)
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'tools/coqdoc/output.ml')
-rw-r--r--tools/coqdoc/output.ml7
1 files changed, 5 insertions, 2 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 06030c45..8589f94a 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -197,8 +197,11 @@ module Latex = struct
printf "\n";
printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n";
printf "%%interpret utf8 characters but extra packages might have to be added\n";
- printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n";
- printf "%%Use coqdoc's option -p to add new packages.\n";
+ printf "%%such as \"textgreek\" for Greek letters not already in tipa\n";
+ printf "%%or \"stmaryrd\" for mathematical symbols.\n";
+ printf "%%Utf8 codes missing a LaTeX interpretation can be defined by using\n";
+ printf "%%\\DeclareUnicodeCharacter{code}{interpretation}.\n";
+ printf "%%Use coqdoc's option -p to add new packages or declarations.\n";
printf "\\usepackage{tipa}\n";
printf "\n"