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 /doc | |
parent | 4249ab5cac5bb0d638400b14c389ded98b3c8ea8 (diff) |
Use the url package, since coqdoc generates \url commands.
Diffstat (limited to 'doc')
-rwxr-xr-x | doc/stdlib/Library.tex | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/stdlib/Library.tex b/doc/stdlib/Library.tex index f410000ea..44a0b1d36 100755 --- a/doc/stdlib/Library.tex +++ b/doc/stdlib/Library.tex @@ -5,6 +5,7 @@ \usepackage[T1]{fontenc} \usepackage{fullpage} \usepackage{amsfonts} +\usepackage{url} \usepackage[color]{../../coqdoc} \input{../common/version} |