diff --git a/src/tools/miri/CONTRIBUTING.md b/src/tools/miri/CONTRIBUTING.md index 073ad267476c..1995300c5bcb 100644 --- a/src/tools/miri/CONTRIBUTING.md +++ b/src/tools/miri/CONTRIBUTING.md @@ -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/ ```