chore: update policy to allow approvals by contributors (#9818)

This adds `allow_contributor: true` which allows approvals by
contributors to the PR (but still not the author themself, which is a
different thing). This allows things like pushing minor fixups while
also approving.

The `ignore_update_merges: true` option makes it so that someone is not
considered a "contributor" just because they push the merge button to
update the branch. In principle this is not needed given the above, but
I like it for clarity.
This commit is contained in:
Jakob Borg 2024-11-12 10:50:19 +01:00 committed by GitHub
parent 1a529e9d5d
commit 896f9725ec
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194

View File

@ -48,6 +48,9 @@ approval_rules:
count: 1
teams:
- syncthing/maintainers
options:
ignore_update_merges: true
allow_contributor: true
# Regular pull requests require approval by an active contributor
- name: is approved by a syncthing contributor
@ -55,6 +58,9 @@ approval_rules:
count: 1
teams:
- syncthing/contributors
options:
ignore_update_merges: true
allow_contributor: true
# Changes to some files (translations, dependencies, compatibility) do not
# require approval if they were proposed by a contributor and have a