user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

gitconfig is not a toml file

Browse source
This commit is contained in:
Ralf Jung 2025-12-11 17:03:49 +01:00
parent 442b868af7
commit 82118ff316
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tools/miri/CONTRIBUTING.md
View file

@ -351,7 +351,7 @@ you need to pull rustc changes into Miri first, and then re-do the rustc push.
If this fails due to authentication problems, it can help to make josh push via ssh instead of
https. Add the following to your `.gitconfig`:
```toml
```text
[url "git@github.com:"]
pushInsteadOf = https://github.com/
```