aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-12 13:06:30 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-03-15 00:07:23 +0100
commit9e2a3531f2e82038f74cd5543eeef7418c494a28 (patch)
tree46a1a3479cfa480a846fc769c70939da9309c988 /doc
parenteb94a77306868504f14926457528ce1b1c4916e6 (diff)
[Sphinx] Move credits to new infrastructure
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/Reference-Manual.tex1
-rw-r--r--doc/sphinx/credits.rst (renamed from doc/refman/RefMan-pre.tex)0
2 files changed, 0 insertions, 1 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 1bd79d511..4935b70c5 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -85,7 +85,6 @@ Options A and B of the licence are {\em not} elected.}
%END LATEX
%\defaultheaders
-\include{RefMan-pre}% Credits
%BEGIN LATEX
\tableofcontents
diff --git a/doc/refman/RefMan-pre.tex b/doc/sphinx/credits.rst
index 05775bfbe..05775bfbe 100644
--- a/doc/refman/RefMan-pre.tex
+++ b/doc/sphinx/credits.rst