Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Remove git config user.* from GitHub CI
Now that we're using a patched submodule rather than applying patches here, we don't need to fib to git about identity. Thanks to David Chisnall for spotting the oversight.
- Loading branch information