diff options
| author | Oli Scherer <git-spam-no-reply9815368754983@oli-obk.de> | 2023-01-30 09:35:05 +0000 |
|---|---|---|
| committer | Oli Scherer <git-spam-no-reply9815368754983@oli-obk.de> | 2023-01-30 09:35:05 +0000 |
| commit | 8a10a4f79ef818897755b8daf52315c013604d4e (patch) | |
| tree | 7cd77ce215006171117ba2fa5a493f85f57e23df | |
| parent | 3ed2c0aa3138c88e4de77d04ca1832848881b28f (diff) | |
| download | rust-8a10a4f79ef818897755b8daf52315c013604d4e.tar.gz rust-8a10a4f79ef818897755b8daf52315c013604d4e.zip | |
Add a note for using ssh login with josh
| -rw-r--r-- | src/tools/miri/CONTRIBUTING.md | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/tools/miri/CONTRIBUTING.md b/src/tools/miri/CONTRIBUTING.md index 5b538691de1..f1bbf16fc7a 100644 --- a/src/tools/miri/CONTRIBUTING.md +++ b/src/tools/miri/CONTRIBUTING.md @@ -242,6 +242,14 @@ josh-proxy --local=$HOME/.cache/josh --remote=https://github.com --no-background This uses a directory `$HOME/.cache/josh` as a cache, to speed up repeated pulling/pushing. +Note that josh is unable to handle ssh auth natively, but you can force it to use ssh auth +by adding the following to your `.gitconfig`: + +```toml +[url "git@github.com:"] + pushInsteadOf = https://github.com/ +``` + ### Importing changes from the rustc repo Josh needs to be running, as described above. |