From 846a303c84703da076dfca2e2b1a9bbb70dc697a Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Tue, 25 Sep 2018 10:43:42 +0200
Subject: [doc] Change Sphinx project title back to "Coq"

Use 'The Coq Reference Manual' only in LaTeX.
---
 doc/sphinx/conf.py | 4 ++--
 1 file 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.
-- 
cgit v1.2.3