aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xdoc/sphinx/conf.py4
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index b43d5fb6f0..71f01cbb17 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -106,7 +106,7 @@ def setup(app):
master_doc = "index"
# General information about the project.
-project = 'The Coq Reference Manual'
+project = 'Coq'
copyright = '1999-2018, Inria'
author = 'The Coq Development Team'
@@ -335,7 +335,7 @@ latex_additional_files = [
"_static/coqnotations.sty"
]
-latex_documents = [('index', 'CoqRefMan.tex', project, author, 'manual')]
+latex_documents = [('index', 'CoqRefMan.tex', 'The Coq Reference Manual', author, 'manual')]
# The name of an image file (relative to this directory) to place at the top of
# the title page.