Downgrade plv8 for Postgres 14/15 #2395
Workflow file for this run
This file contains 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: Handle `approved-for-ci-run` label | |
| # This workflow helps to run CI pipeline for PRs made by external contributors (from forks). | |
| on: | |
| pull_request_target: | |
| branches: | |
| - main | |
| types: | |
| # Default types that triggers a workflow ([1]): | |
| # - [1] https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#pull_request | |
| - opened | |
| - synchronize | |
| - reopened | |
| # Types that we wand to handle in addition to keep labels tidy: | |
| - closed | |
| # Actual magic happens here: | |
| - labeled | |
| concurrency: | |
| group: ${{ github.workflow }}-${{ github.event.pull_request.number }} | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| PR_NUMBER: ${{ github.event.pull_request.number }} | |
| BRANCH: "ci-run/pr-${{ github.event.pull_request.number }}" | |
| # No permission for GITHUB_TOKEN by default; the **minimal required** set of permissions should be granted in each job. | |
| permissions: {} | |
| defaults: | |
| run: | |
| shell: bash -euo pipefail {0} | |
| jobs: | |
| remove-label: | |
| # Remove `approved-for-ci-run` label if the workflow is triggered by changes in a PR. | |
| # The PR should be reviewed and labelled manually again. | |
| permissions: | |
| pull-requests: write # For `gh pr edit` | |
| if: | | |
| contains(fromJSON('["opened", "synchronize", "reopened", "closed"]'), github.event.action) && | |
| contains(github.event.pull_request.labels.*.name, 'approved-for-ci-run') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - run: gh pr --repo "${GITHUB_REPOSITORY}" edit "${PR_NUMBER}" --remove-label "approved-for-ci-run" | |
| create-or-update-pr-for-ci-run: | |
| # Create local PR for an `approved-for-ci-run` labelled PR to run CI pipeline in it. | |
| permissions: | |
| pull-requests: write # for `gh pr edit` | |
| # For `git push` and `gh pr create` we use CI_ACCESS_TOKEN | |
| if: | | |
| github.event.action == 'labeled' && | |
| contains(github.event.pull_request.labels.*.name, 'approved-for-ci-run') | |
| runs-on: ubuntu-latest | |
| steps: | |
| - run: gh pr --repo "${GITHUB_REPOSITORY}" edit "${PR_NUMBER}" --remove-label "approved-for-ci-run" | |
| - uses: actions/checkout@v3 | |
| with: | |
| ref: main | |
| token: ${{ secrets.CI_ACCESS_TOKEN }} | |
| - run: gh pr checkout "${PR_NUMBER}" | |
| - run: git checkout -b "${BRANCH}" | |
| - run: git push --force origin "${BRANCH}" | |
| - name: Create a Pull Request for CI run (if required) | |
| env: | |
| GH_TOKEN: ${{ secrets.CI_ACCESS_TOKEN }} | |
| run: | | |
| cat << EOF > body.md | |
| This Pull Request is created automatically to run the CI pipeline for #${PR_NUMBER} | |
| Please do not alter or merge/close it. | |
| Feel free to review/comment/discuss the original PR #${PR_NUMBER}. | |
| EOF | |
| ALREADY_CREATED="$(gh pr --repo ${GITHUB_REPOSITORY} list --head ${BRANCH} --base main --json number --jq '.[].number')" | |
| if [ -z "${ALREADY_CREATED}" ]; then | |
| gh pr --repo "${GITHUB_REPOSITORY}" create --title "CI run for PR #${PR_NUMBER}" \ | |
| --body-file "body.md" \ | |
| --head "${BRANCH}" \ | |
| --base "main" \ | |
| --draft | |
| fi | |
| cleanup: | |
| # Close PRs and delete branchs if the original PR is closed. | |
| permissions: | |
| contents: write # for `--delete-branch` flag in `gh pr close` | |
| pull-requests: write # for `gh pr close` | |
| if: | | |
| github.event.action == 'closed' && | |
| github.event.pull_request.head.repo.full_name != github.repository | |
| runs-on: ubuntu-latest | |
| steps: | |
| - name: Close PR and delete `ci-run/pr-${{ env.PR_NUMBER }}` branch | |
| run: | | |
| CLOSED="$(gh pr --repo ${GITHUB_REPOSITORY} list --head ${BRANCH} --json 'closed' --jq '.[].closed')" | |
| if [ "${CLOSED}" == "false" ]; then | |
| gh pr --repo "${GITHUB_REPOSITORY}" close "${BRANCH}" --delete-branch | |
| fi |