From dc4fc036cd361fe0d2943039e75570cf08a90868 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Wed, 16 May 2018 21:22:01 -0400
Subject: [doc] Create a separate index file for the LaTeX build

See https://github.com/sphinx-doc/sphinx/issues/4977 for context.
---
 doc/tools/coqrst/coqdomain.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/tools')

diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index b3641c152b..5834ddaa4f 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -620,12 +620,12 @@ class PreambleDirective(Directive):
 
        .. preamble:: preamble.tex
     """
-
     has_content = False
     required_arguments = 1
     optional_arguments = 0
     final_argument_whitespace = True
     option_spec = {}
+    directive_name = "preamble"
 
     def run(self):
         document = self.state.document
-- 
cgit v1.2.3