aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfilliatr2001-04-09 14:59:49 +0000
committerfilliatr2001-04-09 14:59:49 +0000
commit077544a3aa731338ae6771d0116f22df723d389c (patch)
tree87203d42f34200e6024d2cef143c3b0dc25e26e1
parentfba8b0b43b633d48dba995b1133ce88ef992d2ce (diff)
\usepackage{url}
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8177 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--doc/Reference-Manual.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index 60afdee359..599fa3fe6f 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -1,6 +1,7 @@
\documentclass[11pt,a4paper]{book}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
+\usepackage{url}
\usepackage{verbatim}
\usepackage{palatino}