aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/output.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-29 11:59:11 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-29 11:59:11 +0000
commit62ddbf4c06974bb701dd6b370c6b4d670cb5d7cd (patch)
treee4d7d609af1b03ffa12b7c7c0ce4e08ea06303ca /tools/coqdoc/output.ml
parent97da8221e0097ed365f0a99e4960148424a59734 (diff)
Added checksums to glob files and warned about possibly missing
packages for utf8. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14623 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coqdoc/output.ml')
-rw-r--r--tools/coqdoc/output.ml11
1 files changed, 10 insertions, 1 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 605196d6f..28cd79968 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -177,11 +177,20 @@ module Latex = struct
let push_in_preamble s = Queue.add s preamble
+ let utf8x_extra_support () =
+ 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 "\\usepackage{tipa}\n";
+ printf "\n"
+
let header () =
if !header_trailer then begin
printf "\\documentclass[12pt]{report}\n";
if !inputenc != "" then printf "\\usepackage[%s]{inputenc}\n" !inputenc;
- if !inputenc = "utf8x" then printf "\\usepackage{tipa}\n";
+ if !inputenc = "utf8x" then utf8x_extra_support ();
printf "\\usepackage[T1]{fontenc}\n";
printf "\\usepackage{fullpage}\n";
printf "\\usepackage{coqdoc}\n";