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

Auto merge of #2767 - oli-obk:josh_auth, r=RalfJung

Browse source 
Explain how to make josh authenticate with github via ssh

Without this I was unable to push, even though pushing directly to https without josh works.
This commit is contained in:
bors 2023-01-31 10:56:09 +00:00
commit e57962f4f1
1 changed files with 7 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -242,6 +242,13 @@ 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.
To make josh push via ssh instead of https, you can add 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.