Skip to content

Commit

Permalink
Merge pull request #85006 from Calinou/makerst-index-disallow-page-co…
Browse files Browse the repository at this point in the history
…mments

makerst: Disallow user-contributed notes on the class index page
  • Loading branch information
akien-mga authored Nov 17, 2023
2 parents ad72de5 + c7f6504 commit 80de898
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions doc/tools/make_rst.py
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down

0 comments on commit 80de898

Please sign in to comment.