aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tutorial
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-04-28 16:04:13 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2014-04-28 16:04:13 +0200
commit056a969e5d4cd5752bfccf7797ba46c4bcf0b70d (patch)
tree74ce43c3247534121047af09dc774930bd1c0401 /doc/tutorial
parentffeefb4b969aaa0b6728e701593b79250eac1c25 (diff)
Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)
Diffstat (limited to 'doc/tutorial')
-rwxr-xr-xdoc/tutorial/Tutorial.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 5907edb61..55ef730a5 100755
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -1,6 +1,7 @@
\documentclass[11pt,a4paper]{book}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
+\usepackage{textcomp}
\usepackage{pslatex}
\input{../common/version.tex}