summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-10-06 10:12:20 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-10-06 10:12:20 -0400
commitb6e19884393eb011a2f9f12a78f0baa0a768ace3 (patch)
treeabd011403d330b03b20ab00d62b46166656c074e
parentdfdf7b578706995a4d3d8091ffe3ef51035f9f20 (diff)
parent9510a409d0c718142f583b3528e09dd2e3df85ca (diff)
Merge
-rw-r--r--doc/manual.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 20c78235..d98029af 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1,6 +1,6 @@
\documentclass{article}
\usepackage{fullpage,amsmath,amssymb,proof,url}
-
+\usepackage[T1]{fontenc}
\newcommand{\cd}[1]{\texttt{#1}}
\newcommand{\mt}[1]{\mathsf{#1}}