From eea3bb1633cd1efd569b42ca103a99d4a0896c00 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Sun, 11 Mar 2018 09:46:39 +0100
Subject: [Sphinx] Remove information for .chm backend

---
 doc/sphinx/conf.py | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py
index 0bff41a259..0b241fd5b5 100755
--- a/doc/sphinx/conf.py
+++ b/doc/sphinx/conf.py
@@ -230,9 +230,6 @@ html_use_smartypants = False # FIXME wrap code in <code> tags, otherwise quotesg
 # implements a search results scorer. If empty, the default will be used.
 #html_search_scorer = 'scorer.js'
 
-# Output file base name for HTML help builder.
-htmlhelp_basename = 'Coq85doc'
-
 # -- Options for LaTeX output ---------------------------------------------
 
 ###########################
-- 
cgit v1.2.3