[Refinement Types] Add a link to the discussion #6
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: merge-pr-to-main-reminder | |
| on: | |
| pull_request: | |
| types: [opened] | |
| jobs: | |
| merge-pr-to-main-reminder: | |
| name: merge-pr-to-main-reminder | |
| runs-on: ubuntu-latest | |
| permissions: | |
| pull-requests: write | |
| steps: | |
| - name: merge-pr-to-main-reminder | |
| run: | | |
| set -e # Exit if one of commands exit with non-zero exit code | |
| set -u # Treat unset variables and parameters other than the special parameters ‘@’ or ‘*’ as an error | |
| set -o pipefail # Any command failed in the pipe fails the whole pipe | |
| author="$(gh pr view "$PR" --json author --jq '.author.login')" | |
| permissions="$(gh api -H "Accept: application/vnd.github+json" "/repos/Kotlin/KEEP/collaborators/$author/permission" -q .permission)" | |
| if test "$permissions" = admin || test "$permissions" = write || test "$permissions" = maintain; then | |
| gh pr close "$PR" --comment "Please merge your proposal directly to the 'main' branch before opening a public KEEP discussion." | |
| fi | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| GH_REPO: ${{ github.repository }} | |
| PR: ${{ github.event.pull_request.number }} |