diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-10-27 10:08:56 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-10-27 10:32:11 +0100 |
| commit | a9630535a1bbbef0a91795a8136d67fc636a9a93 (patch) | |
| tree | d5cda6c13ab4345497e6c52241f01f1e7461075f /tools/coqdoc | |
| parent | 4249ab5cac5bb0d638400b14c389ded98b3c8ea8 (diff) | |
Use the url package, since coqdoc generates \url commands.
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/output.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 0561d9a08..67a28bfd7 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -211,6 +211,7 @@ module Latex = struct printf "\\usepackage{fullpage}\n"; printf "\\usepackage{coqdoc}\n"; printf "\\usepackage{amsmath,amssymb}\n"; + printf "\\usepackage{url}\n"; (match !toc_depth with | None -> () | Some n -> printf "\\setcounter{tocdepth}{%i}\n" n); |