diff options
| author | Clément Pit-Claudel | 2018-09-06 16:42:24 -0400 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-20 10:12:55 +0200 |
| commit | b627c7242d71c834e7a06353ced967c43598e344 (patch) | |
| tree | 00e139857dc60f48163ca3b71ee44a2272fbaa54 | |
| parent | 7eced434fb9ceafc2d6e248aa5e49bbd6cd2e1fa (diff) | |
[doc] Create a wrapper around the Credits file for the LaTeX build
| -rw-r--r-- | .gitignore | 1 | ||||
| -rw-r--r-- | doc/sphinx/credits-wrapper.html.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/credits-wrapper.latex.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/credits.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/index.html.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/index.latex.rst | 2 |
6 files changed, 13 insertions, 4 deletions
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 ------- |