diff options
author | Hugo Locurcio <hugo.locurcio@hugo.pro> | 2023-11-17 10:51:29 +0100 |
---|---|---|
committer | Hugo Locurcio <hugo.locurcio@hugo.pro> | 2023-11-17 10:51:29 +0100 |
commit | c7f650410526a75594868ea0e2854dc68b2d607e (patch) | |
tree | c65d749d59acfb9b2a95a091bca09e37e8a6b1a5 | |
parent | ad72de508363ca8d10c6b148be44a02cdf12be13 (diff) | |
download | redot-engine-c7f650410526a75594868ea0e2854dc68b2d607e.tar.gz |
makerst: Disallow user-contributed notes on the class index page
User-contributed notes are still allowed on individual class pages.
-rwxr-xr-x | doc/tools/make_rst.py | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/tools/make_rst.py b/doc/tools/make_rst.py index 6db11e4b29..6a99bfbe06 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. |