Merge branch 'develop' into rel_import_categories

sagemath · Nov 1, 2023 · 08ab87a · 08ab87a
2 parents bac9d7c + eb8417b
commit 08ab87a
Show file tree

Hide file tree

Showing 1,040 changed files with 11,517 additions and 10,604 deletions.
diff --git a/.ci/retrofit-worktree.sh b/.ci/retrofit-worktree.sh
@@ -12,6 +12,10 @@ export GIT_AUTHOR_EMAIL="ci-sage@example.com"
 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