From c7f650410526a75594868ea0e2854dc68b2d607e Mon Sep 17 00:00:00 2001 From: Hugo Locurcio Date: Fri, 17 Nov 2023 10:51:29 +0100 Subject: [PATCH] makerst: Disallow user-contributed notes on the class index page User-contributed notes are still allowed on individual class pages. --- doc/tools/make_rst.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/doc/tools/make_rst.py b/doc/tools/make_rst.py index 6db11e4b29a7..6a99bfbe0605 100755 --- a/doc/tools/make_rst.py +++ b/doc/tools/make_rst.py @@ -1536,8 +1536,9 @@ def make_rst_index(grouped_classes: Dict[str, List[str]], dry_run: bool, output_ else: f = open(os.path.join(output_dir, "index.rst"), "w", encoding="utf-8") - # Remove the "Edit on Github" button from the online docs page. - f.write(":github_url: hide\n\n") + # Remove the "Edit on Github" button from the online docs page, and disallow user-contributed notes + # on the index page. User-contributed notes are allowed on individual class pages. + f.write(":github_url: hide\n:allow_comments: False\n\n") # Warn contributors not to edit this file directly. # Also provide links to the source files for reference.