mirror of
https://github.com/carbon-language/carbon-lang.git
synced 2026-10-01 06:04:56 +01:00
Jon Ross-Perkins
ed3a81aa08
Wiki can either be "require push access" or "everyone" -- apparently there's no other option. I've set it to "everyone" so that contributors can make edits without needing push access. So the options as I see it are:
- Leave wiki as "everyone" can edit, use this for notifications.
- GitHub doesn't give notifications for wiki edits. This is trying a different approach for notifications.
- Grant push access to a larger group (contributors), don't add CODEOWNERS.
- Not sure this is the right choice because of the implications around merges, but again maybe it'd be fine and we can expect the approval requirement to work out.
- Grant push access to contributors, add CODEOWNERS.
- This causes the auto-assignment to CODEOWNERS that we don't want. (details in https://github.com/carbon-language/carbon-lang/pull/1367)
- Create a separate wiki repo so that we can differently handle push access.
- This seems overly complex a solution though.
I'm hoping this approach works.
16 lines
445 B
YAML
16 lines
445 B
YAML
# Part of the Carbon Language project, under the Apache License v2.0 with LLVM
|
|
# Exceptions. See /LICENSE for license information.
|
|
# SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
|
|
|
name: Wiki Changed Discord Notification
|
|
|
|
on: gollum
|
|
|
|
jobs:
|
|
notify:
|
|
runs-on: ubuntu-latest
|
|
steps:
|
|
- uses: 'oznu/gh-wiki-edit-discord-notification@v1.0.0'
|
|
with:
|
|
discord-webhook-url: ${{ secrets.DISCORD_WEBHOOK_WIKI_EDIT }}
|