diff options
| author | bors <bors@rust-lang.org> | 2022-11-15 16:24:10 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2022-11-15 16:24:10 +0000 |
| commit | a046f62bb4230549dd5085e836705d6fe3ca86b3 (patch) | |
| tree | 7cf1cba0eb258b0fae2238954920e97b4a71369f | |
| parent | c6649aafc65f6feb96414767395a498707118496 (diff) | |
| parent | 3c72492e3e04362e9b576f4f2e0fc70562c1d409 (diff) | |
| download | rust-a046f62bb4230549dd5085e836705d6fe3ca86b3.tar.gz rust-a046f62bb4230549dd5085e836705d6fe3ca86b3.zip | |
Auto merge of #2666 - RalfJung:josh, r=RalfJung
update josh instructions https://github.com/josh-project/josh/pull/965 and https://github.com/josh-project/josh/pull/994 have been merged so we don't need a forked josh any more. :) However, this is blocked on https://github.com/josh-project/josh/issues/1032 which currently prevents me from actually testing this...
| -rw-r--r-- | src/tools/miri/CONTRIBUTING.md | 8 | ||||
| -rwxr-xr-x | src/tools/miri/miri | 4 |
2 files changed, 6 insertions, 6 deletions
diff --git a/src/tools/miri/CONTRIBUTING.md b/src/tools/miri/CONTRIBUTING.md index f0f0cb20317..1c3d9d3fc40 100644 --- a/src/tools/miri/CONTRIBUTING.md +++ b/src/tools/miri/CONTRIBUTING.md @@ -283,13 +283,13 @@ 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, a fork of josh needs to be built -from source. This downloads and runs josh: +changes between the rustc and Miri repositories. For now, the latest git version +of josh needs to be built from source. This downloads and runs josh: ```sh -git clone https://github.com/RalfJung/josh +git clone https://github.com/josh-project/josh cd josh -cargo run --release -p josh-proxy -- --local=$(pwd)/local --remote=https://github.com --no-background +cargo run --release -p josh-proxy -- --local=local --remote=https://github.com --no-background ``` ### Importing changes from the rustc repo diff --git a/src/tools/miri/miri b/src/tools/miri/miri index f0986bfb1cd..fd2eaa42b7b 100755 --- a/src/tools/miri/miri +++ b/src/tools/miri/miri @@ -78,7 +78,7 @@ shift # macOS does not have a useful readlink/realpath so we have to use Python instead... MIRIDIR=$(python3 -c 'import os, sys; print(os.path.dirname(os.path.realpath(sys.argv[1])))' "$0") # Used for rustc syncs. -JOSH_FILTER=":at_commit=75dd959a3a40eb5b4574f8d2e23aa6efbeb33573[:prefix=src/tools/miri]:/src/tools/miri" +JOSH_FILTER=":rev(75dd959a3a40eb5b4574f8d2e23aa6efbeb33573:prefix=src/tools/miri):/src/tools/miri" # Needed for `./miri bench`. TOOLCHAIN=$(cd "$MIRIDIR"; rustup show active-toolchain | head -n 1 | cut -d ' ' -f 1) @@ -149,7 +149,7 @@ rustc-push) # and set `-o base` to a branch that holds current rustc master. echo "Preparing $USER/rust..." if git fetch https://github.com/$USER/rust $BRANCH &>/dev/null; then - echo "The '$BRANCH' seems to already exist in $USER/rust. Please delete it and try again." + echo "The branch '$BRANCH' seems to already exist in $USER/rust. Please delete it and try again." exit 1 fi git fetch https://github.com/rust-lang/rust master |