From 7eced434fb9ceafc2d6e248aa5e49bbd6cd2e1fa Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Mon, 13 Aug 2018 18:27:20 -0400
Subject: [doc] Create a separate zebibliography file for the LaTeX build

`.. bibliography::` puts the bibliography on its own page with its own title in
LaTeX, but includes it inline without a title in HTML [1], so we need to
maintain two separate copies of zebibliography.rst

[1] https://sphinxcontrib-bibtex.readthedocs.io/en/latest/usage.html#mismatch-between-output-of-html-and-latex-backends
---
 .gitignore | 1 +
 1 file changed, 1 insertion(+)

(limited to '.gitignore')

diff --git a/.gitignore b/.gitignore
index 8c5d8bcc16..d52898b3a5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -100,6 +100,7 @@ doc/faq/axioms.eps_t
 doc/faq/axioms.pdf_t
 doc/faq/axioms.png
 doc/sphinx/index.rst
+doc/sphinx/zebibliography.rst
 doc/stdlib/Library.out
 doc/stdlib/Library.ps
 doc/stdlib/Library.coqdoc.tex
-- 
cgit v1.2.3