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

Update CONTRIBUTING.md

Browse source 
Co-authored-by: Ralf Jung <post@ralfj.de>
This commit is contained in:
Oli Scherer 2023-01-31 11:27:08 +01:00 • committed by GitHub
parent 8a10a4f79e
commit 247a5f3aca
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -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:"]