diff options
| author |  Johannes Christ <[email protected]> | 2024-07-29 19:22:20 +0200 |
|---|---|---|
| committer | Johannes Christ <[email protected]> | 2024-07-30 19:50:01 +0200 |
| commit | 0c8ff754360b6fbc623f12613238e0e6ccd0ed42 (patch) | |
| tree | 57a0f3e5e878c425f5b078861a3664c58b53e3b5 /docs | |
| parent | Do not include all children sections on postmortem TOC (diff) | |
Clean up some wording and formatting issues
Diffstat (limited to 'docs')
| -rw-r--r-- | docs/tooling/bots.rst | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/docs/tooling/bots.rst b/docs/tooling/bots.rst index e38f83c..7b5e165 100644 --- a/docs/tooling/bots.rst +++ b/docs/tooling/bots.rst @@ -1,13 +1,16 @@ +Bots +==== + Our GitHub repositories are supported by two custom bots: - Our **Fast Forward Bot**, which ensures that commits merged into main are either merged manually on the command line or via a fast-forward, ensuring that cryptographic signatures of commits remain intact. - Information on the bot can be found `in the ``ff-bot.yml`` + Information on the bot can be found `in the ff-bot.yml configuration <https://github.com/python-discord/infra/blob/main/.github/ff-bot.yml>`__. Merges over the GitHub UI are discouraged for this reason. You can use it by running ``/merge`` on a pull request. Note that attempting - to use it without permission to will be reported. + to use it without permission to do so will be reported. - Our **Craig Dazey Emulator Bot**, which ensures team morale stays high at all times by thanking team members for submitted pull |