Merge remote-tracking branch 'origin/develop' into rel_headers

Author: tobiasdiez

.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