diff options
| author | Ralf Jung <post@ralfj.de> | 2022-10-24 08:05:52 +0200 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2022-10-24 08:05:52 +0200 |
| commit | 0d0a603aaba085f31d7639dcbf6b460f7d1766cf (patch) | |
| tree | e1628ebab55dc181932f4e8f677aeaea82783b23 | |
| parent | 233542bf424af3153f031cdc54c010959e1bb403 (diff) | |
| download | rust-0d0a603aaba085f31d7639dcbf6b460f7d1766cf.tar.gz rust-0d0a603aaba085f31d7639dcbf6b460f7d1766cf.zip | |
point to my fork of josh for now
| -rw-r--r-- | src/tools/miri/CONTRIBUTING.md | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/tools/miri/CONTRIBUTING.md b/src/tools/miri/CONTRIBUTING.md index c9a7d708f1e..b1e6b9c69d3 100644 --- a/src/tools/miri/CONTRIBUTING.md +++ b/src/tools/miri/CONTRIBUTING.md @@ -279,13 +279,12 @@ With this, you should now have a working development setup! See ## Advanced topic: Syncing with the rustc repo We use the [`josh` proxy](https://github.com/josh-project/josh) to transmit -changes between the rustc and Miri repositories. For now, josh needs to be built +changes between the rustc and Miri repositories. For now, a fork of josh needs to be built from source. This downloads and runs josh: ```sh -git clone https://github.com/josh-project/josh +git clone https://github.com/RalfJung/josh cd josh -git checkout @changes/master/christian.schilling.de@gmail.com/start-filter cargo run --release -p josh-proxy -- --local=$(pwd)/local --remote=https://github.com --no-background ``` |