diff options
| author | Clément Pit-Claudel | 2018-05-16 21:22:01 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | dc4fc036cd361fe0d2943039e75570cf08a90868 (patch) | |
| tree | fb2a92d7b99504dc2c7cdaae6f8228d755a4a4c7 /doc/tools | |
| parent | 6146def665803be4f37eedee0d81b2f807e1b3f7 (diff) | |
[doc] Create a separate index file for the LaTeX build
See https://github.com/sphinx-doc/sphinx/issues/4977 for context.
Diffstat (limited to 'doc/tools')
| -rw-r--r-- | doc/tools/coqrst/coqdomain.py | 2 |
1 files changed, 1 insertions, 1 deletions
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 |