diff options
| author | Guillaume Melquiond | 2014-10-27 10:08:56 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2014-10-27 10:32:11 +0100 |
| commit | a9630535a1bbbef0a91795a8136d67fc636a9a93 (patch) | |
| tree | d5cda6c13ab4345497e6c52241f01f1e7461075f /dev/include | |
| parent | 4249ab5cac5bb0d638400b14c389ded98b3c8ea8 (diff) | |
Use the url package, since coqdoc generates \url commands.
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions