diff options
| author | Maxime Dénès | 2018-03-11 09:46:39 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-13 12:45:30 +0100 |
| commit | eea3bb1633cd1efd569b42ca103a99d4a0896c00 (patch) | |
| tree | 012b0677bf40177bd016202cab12ad51c0740681 /doc | |
| parent | 586fba203e7ce0b56d364c2e30b30bb02dec4905 (diff) | |
[Sphinx] Remove information for .chm backend
Diffstat (limited to 'doc')
| -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 --------------------------------------------- ########################### |