CI: checkout HEAD commit rather than merge commit
GitHub CI actions/checkout uses a merge commit which isn't compatible with our formality checks. Instead checkout the pull request HEAD. Signed-off-by: Paul Spooren <mail@aparcar.org>
This commit is contained in:
parent
fa631e9284
commit
13c1f2bcda
1 changed files with 1 additions and 3 deletions
4
.github/workflows/formal.yml
vendored
4
.github/workflows/formal.yml
vendored
|
@ -13,6 +13,7 @@ jobs:
|
||||||
steps:
|
steps:
|
||||||
- uses: actions/checkout@v2
|
- uses: actions/checkout@v2
|
||||||
with:
|
with:
|
||||||
|
ref: ${{ github.event.pull_request.head.sha }}
|
||||||
fetch-depth: 0
|
fetch-depth: 0
|
||||||
|
|
||||||
- name: Determine branch name
|
- name: Determine branch name
|
||||||
|
@ -23,9 +24,6 @@ jobs:
|
||||||
|
|
||||||
- name: Test formalities
|
- name: Test formalities
|
||||||
run: |
|
run: |
|
||||||
# remove GitHubs merge commit
|
|
||||||
git rebase "origin/$BRANCH"
|
|
||||||
|
|
||||||
source .github/workflows/ci_helpers.sh
|
source .github/workflows/ci_helpers.sh
|
||||||
|
|
||||||
RET=0
|
RET=0
|
||||||
|
|
Loading…
Reference in a new issue