diff options
| author | Oli Scherer <github35764891676564198441@oli-obk.de> | 2023-01-31 11:27:08 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2023-01-31 11:27:08 +0100 |
| commit | 247a5f3acaee6cdd38476d7d558de2ac0f11489d (patch) | |
| tree | 53cbb0e02878ab866826a0b904040a123d6cf8ef | |
| parent | 8a10a4f79ef818897755b8daf52315c013604d4e (diff) | |
| download | rust-247a5f3acaee6cdd38476d7d558de2ac0f11489d.tar.gz rust-247a5f3acaee6cdd38476d7d558de2ac0f11489d.zip | |
Update CONTRIBUTING.md
Co-authored-by: Ralf Jung <post@ralfj.de>
| -rw-r--r-- | src/tools/miri/CONTRIBUTING.md | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/tools/miri/CONTRIBUTING.md b/src/tools/miri/CONTRIBUTING.md index f1bbf16fc7a..476075e9c91 100644 --- a/src/tools/miri/CONTRIBUTING.md +++ b/src/tools/miri/CONTRIBUTING.md @@ -242,8 +242,7 @@ 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`: +To make josh push via ssh instead of https, you can add the following to your `.gitconfig`: ```toml [url "git@github.com:"] |