Skip to content

modified: .github/workflows/master-pr.yml #478

modified: .github/workflows/master-pr.yml

modified: .github/workflows/master-pr.yml #478

Workflow file for this run

name: 'Test PR'
on:
pull_request:
branches:
- 'master'
concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true
jobs:
change-base:
name: 'Change base to develop branch'
runs-on: ubuntu-24.04
permissions:
pull-requests: write
steps:
- name: 'Check out code'
uses: actions/checkout@v4
with:
fetch-depth: 0
- name: 'Change base'
env:
GITHUB_TOKEN: ${{ github.token }}
run: |
set -x
pull_number=$(jq --raw-output .pull_request.number "${GITHUB_EVENT_PATH}")
curl -X PATCH \
-H "Accept: application/vnd.github+json" \
-H "Authorization: Bearer ${GITHUB_TOKEN}" \
"https://api.github.com/repos/runtimeverification/k/pulls/${pull_number}" \
-d '{"base":"develop"}'
- name: 'Post comment about base change'
env:
GITHUB_TOKEN: ${{ github.token }}
run: |
set -x
pull_number=$(jq --raw-output .pull_request.number "${GITHUB_EVENT_PATH}")
comment_body='The default branch has been changed from master to develop. Thank you for your support!'
curl -X POST \
-H "Accept: application/vnd.github+json" \
-H "Authorization: Bearer ${GITHUB_TOKEN}" \
"https://api.github.com/repos/runtimeverification/k/issues/${pull_number}/comments" \
-d "{\"body\":\"${comment_body}\"}"