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

Add a note for using ssh login with josh

Browse source
This commit is contained in:
Oli Scherer 2023-01-30 09:35:05 +00:00
parent 3ed2c0aa31
commit 8a10a4f79e
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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.