diff options
| author | Rémi Verschelde <remi@verschelde.fr> | 2023-11-17 12:43:54 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-11-17 12:43:54 +0100 |
| commit | 80de898d721f952dac0b102d48bb73d6b02ee1e8 (patch) | |
| tree | c65d749d59acfb9b2a95a091bca09e37e8a6b1a5 | |
| parent | ad72de508363ca8d10c6b148be44a02cdf12be13 (diff) | |
| parent | c7f650410526a75594868ea0e2854dc68b2d607e (diff) | |
| download | redot-engine-80de898d721f952dac0b102d48bb73d6b02ee1e8.tar.gz | |
Merge pull request #85006 from Calinou/makerst-index-disallow-page-comments
makerst: Disallow user-contributed notes on the class index page
| -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. |