summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-01-19 22:34:29 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-01-19 22:34:29 +0000
commit018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch)
treefbb91e2f74c73bb867ab62c58f248a704bbe6dec /tools
parent6497f27021fec4e01f2182014f2bb1989b4707f9 (diff)
Imported Upstream version 8.0pl3upstream/8.0pl3
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/coqdoc.sty4
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index 7f7aa9aa..68b9ab26 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -16,8 +16,8 @@
\pagestyle{fancyplain}
%BEGIN LATEX
-\plainheadrulewidth 0.4pt
-\plainfootrulewidth 0pt
+\renewcommand{\plainheadrulewidth}{0.4pt}
+\renewcommand{\plainfootrulewidth}{0pt}
\lhead[\coqdocleftpageheader]{\leftmark}
\rhead[\leftmark]{\coqdocrightpageheader}
\cfoot{}