From b627c7242d71c834e7a06353ced967c43598e344 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Thu, 6 Sep 2018 16:42:24 -0400
Subject: [doc] Create a wrapper around the Credits file for the LaTeX build

---
 .gitignore                           | 1 +
 doc/sphinx/credits-wrapper.html.rst  | 7 +++++++
 doc/sphinx/credits-wrapper.latex.rst | 3 +++
 doc/sphinx/credits.rst               | 2 --
 doc/sphinx/index.html.rst            | 2 +-
 doc/sphinx/index.latex.rst           | 2 +-
 6 files changed, 13 insertions(+), 4 deletions(-)
 create mode 100644 doc/sphinx/credits-wrapper.html.rst
 create mode 100644 doc/sphinx/credits-wrapper.latex.rst

diff --git a/.gitignore b/.gitignore
index d52898b3a5..582a8f43c7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -101,6 +101,7 @@ doc/faq/axioms.pdf_t
 doc/faq/axioms.png
 doc/sphinx/index.rst
 doc/sphinx/zebibliography.rst
+doc/sphinx/credits-wrapper.rst
 doc/stdlib/Library.out
 doc/stdlib/Library.ps
 doc/stdlib/Library.coqdoc.tex
diff --git a/doc/sphinx/credits-wrapper.html.rst b/doc/sphinx/credits-wrapper.html.rst
new file mode 100644
index 0000000000..2d35a12dc2
--- /dev/null
+++ b/doc/sphinx/credits-wrapper.html.rst
@@ -0,0 +1,7 @@
+.. _credits:
+
+-------
+Credits
+-------
+
+.. include:: credits.rst
diff --git a/doc/sphinx/credits-wrapper.latex.rst b/doc/sphinx/credits-wrapper.latex.rst
new file mode 100644
index 0000000000..9f7dd49af8
--- /dev/null
+++ b/doc/sphinx/credits-wrapper.latex.rst
@@ -0,0 +1,3 @@
+.. _credits:
+
+.. include:: credits.rst
diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst
index 62851039bf..be6fe5704e 100644
--- a/doc/sphinx/credits.rst
+++ b/doc/sphinx/credits.rst
@@ -1,5 +1,3 @@
-.. _credits:
-
 Coq is a proof assistant for higher-order logic, allowing the
 development of computer programs consistent with their formal
 specification. It is the result of about ten years of research of the
diff --git a/doc/sphinx/index.html.rst b/doc/sphinx/index.html.rst
index b96a01f76d..96ddd27027 100644
--- a/doc/sphinx/index.html.rst
+++ b/doc/sphinx/index.html.rst
@@ -28,7 +28,7 @@ Table of contents
    :caption: Preamble
 
    self
-   credits
+   credits-wrapper
 
 .. toctree::
    :caption: The language
diff --git a/doc/sphinx/index.latex.rst b/doc/sphinx/index.latex.rst
index 13bc1a19e7..0f2f7b4897 100644
--- a/doc/sphinx/index.latex.rst
+++ b/doc/sphinx/index.latex.rst
@@ -10,7 +10,7 @@ Introduction
 Credits
 -------
 
-.. include:: credits.rst
+.. include:: credits-wrapper.rst
 
 License
 -------
-- 
cgit v1.2.3