diff options
| -rwxr-xr-x | src/tools/miri/miri | 2 | ||||
| -rw-r--r-- | src/tools/miri/rust-version | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/tools/miri/miri b/src/tools/miri/miri index 52902410a6b..a0593deb08a 100755 --- a/src/tools/miri/miri +++ b/src/tools/miri/miri @@ -121,7 +121,7 @@ toolchain) rustc-pull) cd "$MIRIDIR" git fetch http://localhost:8000/rust-lang/rust.git$JOSH_FILTER.git master - git merge FETCH_HEAD + git merge FETCH_HEAD --no-ff -m "Merge from rustc" exit 0 ;; rustc-push) diff --git a/src/tools/miri/rust-version b/src/tools/miri/rust-version index e582bf35356..13492d183c9 100644 --- a/src/tools/miri/rust-version +++ b/src/tools/miri/rust-version @@ -1 +1 @@ -607878d069267e1402ad792c9331b426e4c6d0f9 +b03502b35d111bef0399a66ab3cc765f0802e8ba |