Merge branch 'develop' into rel_import_small

tobiasdiez · Nov 5, 2023 · e8c3d6e · e8c3d6e
2 parents 289d658 + ebef87a
commit e8c3d6e
Show file tree

Hide file tree

Showing 1,549 changed files with 22,086 additions and 18,910 deletions.
diff --git a/.ci/merge-fixes.sh b/.ci/merge-fixes.sh
@@ -14,10 +14,10 @@ else
     git tag -f test_base
     git commit -q -m "Uncommitted changes" --no-allow-empty -a
     for a in $PRs; do
+        git fetch --unshallow --all > /dev/null 2>&1 && echo "Unshallowed."
         echo "::group::Merging PR https://github.com/$REPO/pull/$a"
         git tag -f test_head
         $GH pr checkout -b pr-$a $a
-        git fetch --unshallow --all
         git checkout -q test_head
         if git merge --no-edit --squash -q pr-$a; then
             echo "::endgroup::"

diff --git a/.ci/retrofit-worktree.sh b/.ci/retrofit-worktree.sh
@@ -12,6 +12,10 @@ export GIT_AUTHOR_EMAIL="[email protected]"
 export GIT_COMMITTER_NAME="$GIT_AUTHOR_NAME"
 export GIT_COMMITTER_EMAIL="$GIT_AUTHOR_EMAIL"
 
+# Set globally for other parts of the workflow
+git config --global user.name "$GIT_AUTHOR_NAME"
+git config --global user.email "$GIT_AUTHOR_EMAIL"
+
 set -ex
 
 # If actions/checkout downloaded our source tree using the GitHub REST API