Merge branch 'develop' into fix_get_ci_fixes-1

sagemath · Nov 15, 2023 · 20fb5c3 · 20fb5c3
2 parents da5d53d + fa5c939
commit 20fb5c3
Show file tree

Hide file tree

Showing 1,584 changed files with 22,465 additions and 19,150 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 --allow-unrelated-histories -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