aboutsummaryrefslogtreecommitdiff
path: root/doc/faq/FAQ.tex
diff options
context:
space:
mode:
authorGuillaume Melquiond2014-04-28 16:04:13 +0200
committerGuillaume Melquiond2014-04-28 16:04:13 +0200
commit056a969e5d4cd5752bfccf7797ba46c4bcf0b70d (patch)
tree74ce43c3247534121047af09dc774930bd1c0401 /doc/faq/FAQ.tex
parentffeefb4b969aaa0b6728e701593b79250eac1c25 (diff)
Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)
Diffstat (limited to 'doc/faq/FAQ.tex')
-rw-r--r--doc/faq/FAQ.tex1
1 files changed, 1 insertions, 0 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index a5536911d7..5806e9d72d 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -7,6 +7,7 @@
\pagestyle{plain}
% yay les symboles
+\usepackage{textcomp}
\usepackage{stmaryrd}
\usepackage{amssymb}
\usepackage{url}