From 82118ff316c67710f1677ae6e36660f7fed91d3a Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 11 Dec 2025 17:03:49 +0100 Subject: [PATCH] gitconfig is not a toml file --- src/tools/miri/CONTRIBUTING.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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/ ```