From ba183ec0375fde7341f343a7b5b9b53cac6ba7bd Mon Sep 17 00:00:00 2001
From: Mikhail Kirilin <kirilin@ins.uni-bonn.de>
Date: Mon, 4 Mar 2024 14:07:09 +0100
Subject: [PATCH] Add head repo remote

---
 .github/workflows/ci_submodule.yml | 24 ++++++++++++++++--------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/.github/workflows/ci_submodule.yml b/.github/workflows/ci_submodule.yml
index d85fc4cb1..3d399c763 100644
--- a/.github/workflows/ci_submodule.yml
+++ b/.github/workflows/ci_submodule.yml
@@ -12,10 +12,19 @@ jobs:
       PR_NODE_ID: ${{ github.event.pull_request.node_id }}
       INPUT_PATH: sc
     steps:
-    - name: Checkout source code
+    - name: Checkout source code for base
       uses: actions/checkout@v4
       with:
         submodules: true
+        path: base
+
+    - name: Checkout source code for head
+      uses: actions/checkout@v4
+      with:
+        repository: ${{ github.event.pull_request.head.repo.full_name }}
+        ref: ${{ github.event.pull_request.head.ref }}
+        submodules: true
+        path: head
         
     - name: Determine hashes to compare
       shell: bash
@@ -24,22 +33,21 @@ jobs:
         cd "${GITHUB_WORKSPACE}" \
         || error "__Line:${LINENO}__Error: Cannot change directory to Github Workspace"
         echo "PR=`jq -r ".number" "${EVENT_PATH}"`" >> $GITHUB_ENV
-        PR_REPO=`jq -r ".pull_request.head.repo" "${EVENT_PATH}"`
         PR_BRANCH=`jq -r ".pull_request.head.ref" "${EVENT_PATH}"`
         BASE_BRANCH=`jq -r ".pull_request.base.ref" "${EVENT_PATH}"`
-        echo "Run for PR of ${PR_REPO}/${PR_BRANCH} into ${BASE_BRANCH}"
-        echo "Fetch Branch Histories"
-        git fetch ${PR_REPO} "${PR_BRANCH}" --recurse-submodules=no \
+        echo "Run for PR of ${PR_BRANCH} into ${BASE_BRANCH}"
+        cd head
+        git fetch origin "${PR_BRANCH}" --recurse-submodules=no \
         || error "__Line:${LINENO}__Error: Could not fetch history of ${PR_BRANCH}"
+        cd ../base
         git fetch origin "${BASE_BRANCH}" --recurse-submodules=no \
         || error "__Line:${LINENO}__Error: Could not fetch history of ${BASE_BRANCH}"
-        echo "TO_HASH=`git rev-parse ${PR_REPO}/${PR_BRANCH}`" >> $GITHUB_ENV
-        echo "FROM_HASH=`git rev-parse origin/${BASE_BRANCH}`" >> $GITHUB_ENV
+        cd ..
 
     - name: Convert PR to draft if necessary
       shell: bash
       run: |
-        CHANGED=`git diff --name-only ${{ env.FROM_HASH }}...${{ env.TO_HASH }}`
+        CHANGED=`git diff --name-only --no-index -- "${GITHUB_WORKSPACE}"/base/ "${GITHUB_WORKSPACE}"/head/` || true
         if grep "^${INPUT_PATH}$" <<< "${CHANGED}"; then
           echo "${TOKEN}" | gh auth login --with-token
           gh pr comment ${PR} --body \