From 13c1f2bcda33ab8fc17ede1f43f60e0aac8b7cab Mon Sep 17 00:00:00 2001
From: Paul Spooren <mail@aparcar.org>
Date: Thu, 4 Mar 2021 23:16:00 -1000
Subject: [PATCH] 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>
---
 .github/workflows/formal.yml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/.github/workflows/formal.yml b/.github/workflows/formal.yml
index 7a7a6b0aa1..25609174e8 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