File tree 2 files changed +6
-6
lines changed
2 files changed +6
-6
lines changed Original file line number Diff line number Diff line change @@ -283,13 +283,13 @@ With this, you should now have a working development setup! See
283
283
## Advanced topic: Syncing with the rustc repo
284
284
285
285
We use the [ ` josh ` proxy] ( https://github.com/josh-project/josh ) to transmit
286
- changes between the rustc and Miri repositories. For now, a fork of josh needs to be built
287
- from source. This downloads and runs josh:
286
+ changes between the rustc and Miri repositories. For now, the latest git version
287
+ of josh needs to be built from source. This downloads and runs josh:
288
288
289
289
``` sh
290
- git clone https://github.com/RalfJung /josh
290
+ git clone https://github.com/josh-project /josh
291
291
cd josh
292
- cargo run --release -p josh-proxy -- --local=$( pwd ) / local --remote=https://github.com --no-background
292
+ cargo run --release -p josh-proxy -- --local=local --remote=https://github.com --no-background
293
293
```
294
294
295
295
### Importing changes from the rustc repo
Original file line number Diff line number Diff line change 78
78
# macOS does not have a useful readlink/realpath so we have to use Python instead...
79
79
MIRIDIR=$( python3 -c ' import os, sys; print(os.path.dirname(os.path.realpath(sys.argv[1])))' " $0 " )
80
80
# Used for rustc syncs.
81
- JOSH_FILTER=" :at_commit= 75dd959a3a40eb5b4574f8d2e23aa6efbeb33573[ :prefix=src/tools/miri] :/src/tools/miri"
81
+ JOSH_FILTER=" :rev( 75dd959a3a40eb5b4574f8d2e23aa6efbeb33573:prefix=src/tools/miri) :/src/tools/miri"
82
82
# Needed for `./miri bench`.
83
83
TOOLCHAIN=$( cd " $MIRIDIR " ; rustup show active-toolchain | head -n 1 | cut -d ' ' -f 1)
84
84
@@ -149,7 +149,7 @@ rustc-push)
149
149
# and set `-o base` to a branch that holds current rustc master.
150
150
echo " Preparing $USER /rust..."
151
151
if git fetch https://github.com/$USER /rust $BRANCH & > /dev/null; then
152
- echo " The '$BRANCH ' seems to already exist in $USER /rust. Please delete it and try again."
152
+ echo " The branch '$BRANCH ' seems to already exist in $USER /rust. Please delete it and try again."
153
153
exit 1
154
154
fi
155
155
git fetch https://github.com/rust-lang/rust master
You can’t perform that action at this time.
0 commit comments