diff options
| author | Paul Spooren <mail@aparcar.org> | 2021-03-04 23:16:00 -1000 |
|---|---|---|
| committer | Paul Spooren <mail@aparcar.org> | 2021-03-04 23:42:32 -1000 |
| commit | 13c1f2bcda33ab8fc17ede1f43f60e0aac8b7cab (patch) | |
| tree | e57a5240557f6053c2a0a97a0fdc0cea7c2206c2 /.github | |
| parent | fa631e92840dfc3fd13951dd56f54761e19ca3e7 (diff) | |
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>
Diffstat (limited to '.github')
| -rw-r--r-- | .github/workflows/formal.yml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml index 7a7a6b0aa..25609174e 100644 --- a/.github/workflows/formal.yml +++ b/.github/workflows/formal.yml @@ -13,6 +13,7 @@ jobs: steps: - uses: actions/checkout@v2 with: + ref: ${{ github.event.pull_request.head.sha }} fetch-depth: 0 - name: Determine branch name @@ -23,9 +24,6 @@ jobs: - name: Test formalities run: | - # remove GitHubs merge commit - git rebase "origin/$BRANCH" - source .github/workflows/ci_helpers.sh RET=0 |