From f4224d402f6c1d6856fbf676461a1da05a1eaccf Mon Sep 17 00:00:00 2001
From: Mikhail Kirilin <kirilin@ins.uni-bonn.de>
Date: Tue, 19 Mar 2024 11:20:36 +0100
Subject: [PATCH] Do not load submodules

---
 .github/workflows/ci_submodule.yml | 21 +++++++++++----------
 1 file changed, 11 insertions(+), 10 deletions(-)

diff --git a/.github/workflows/ci_submodule.yml b/.github/workflows/ci_submodule.yml
index 3d399c763..52ccb13eb 100644
--- a/.github/workflows/ci_submodule.yml
+++ b/.github/workflows/ci_submodule.yml
@@ -5,6 +5,7 @@ on:
 jobs:
 
   linux-sub:
+    permissions: write-all
     if: github.event.pull_request.draft == false
     runs-on: ubuntu-latest
     env:
@@ -15,7 +16,7 @@ jobs:
     - name: Checkout source code for base
       uses: actions/checkout@v4
       with:
-        submodules: true
+        submodules: false
         path: base
 
     - name: Checkout source code for head
@@ -23,7 +24,7 @@ jobs:
       with:
         repository: ${{ github.event.pull_request.head.repo.full_name }}
         ref: ${{ github.event.pull_request.head.ref }}
-        submodules: true
+        submodules: false
         path: head
         
     - name: Determine hashes to compare
@@ -32,28 +33,28 @@ jobs:
         EVENT_PATH="${GITHUB_EVENT_PATH}"
         cd "${GITHUB_WORKSPACE}" \
         || error "__Line:${LINENO}__Error: Cannot change directory to Github Workspace"
-        echo "PR=`jq -r ".number" "${EVENT_PATH}"`" >> $GITHUB_ENV
+        PR=`jq -r ".number" "${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_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}"
+        HEAD_SC_HASH=`git log -n1 sc | awk 'NR==1{ print $2 }'`
         cd ../base
         git fetch origin "${BASE_BRANCH}" --recurse-submodules=no \
         || error "__Line:${LINENO}__Error: Could not fetch history of ${BASE_BRANCH}"
-        cd ..
-
-    - name: Convert PR to draft if necessary
-      shell: bash
-      run: |
-        CHANGED=`git diff --name-only --no-index -- "${GITHUB_WORKSPACE}"/base/ "${GITHUB_WORKSPACE}"/head/` || true
-        if grep "^${INPUT_PATH}$" <<< "${CHANGED}"; then
+        BASE_SC_HASH=`git log -n1 sc | awk 'NR==1{ print $2 }'`
+        echo "HEAD_SC_HASH: $HEAD_SC_HASH, BASE_SC_HASH: $BASE_SC_HASH"
+        if [[ "x$HEAD_SC_HASH"!="x$BASE_SC_HASH" ]]; then
           echo "${TOKEN}" | gh auth login --with-token
+          echo "Login successfully with token ${TOKEN}."
+          echo "PR: $PR"
           gh pr comment ${PR} --body \
           "Submodule has been changed by this PR. \
           This is forbidden by the repository policy. \
           Your PR is turned into a draft PR."
+          echo "PR was commented successfully."
           gh api graphql -F id="${PR_NODE_ID}"  -f query='
             mutation($id: ID!) {
               convertPullRequestToDraft(input: { pullRequestId: $id }) {