diff options
| -rwxr-xr-x | doc/sphinx/conf.py | 3 |
1 files changed, 0 insertions, 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 --------------------------------------------- ########################### |