From 9457085fc838ff7ebe4dd47399a42a76185e62e4 Mon Sep 17 00:00:00 2001 From: Kovid Goyal Date: Sun, 28 Feb 2021 19:59:49 +0530 Subject: [PATCH] Remove no longer needed monkeypatch --- manual/custom.py | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/manual/custom.py b/manual/custom.py index b09a5e5e96..24740816d6 100644 --- a/manual/custom.py +++ b/manual/custom.py @@ -354,24 +354,8 @@ def setup_man_pages(app): app.config['man_pages'] = man_pages -def monkey_patch_docutils(): - # fixes a bug in sphinx https://github.com/sphinx-doc/sphinx/issues/5150 - from docutils import nodes - - orig_method = nodes.document.set_duplicate_name_id - - def set_duplicate_name_id(*a): - try: - return orig_method(*a) - except KeyError: - pass - - nodes.document.set_duplicate_name_id = set_duplicate_name_id - - def setup(app): from docutils.parsers.rst import roles - monkey_patch_docutils() setup_man_pages(app) app.add_css_file('custom.css') app.add_builder(EPUBHelpBuilder)