diff options
| author | bors <bors@rust-lang.org> | 2022-10-06 00:00:29 +0000 |
|---|---|---|
| committer | bors <bors@rust-lang.org> | 2022-10-06 00:00:29 +0000 |
| commit | 27579a214dc2a918e67bffb51a0825005e8bd42e (patch) | |
| tree | 2f61e982831c65eaf3dc69ef001c8b94278664d7 /src/ci/scripts/should-skip-this.sh | |
| parent | c97d02cdb5ca5f5e9eff1fa9e4560d220d1fd2a0 (diff) | |
| parent | 9cc11e262f1c8313ec11154a2d5440ff5664aec4 (diff) | |
| download | rust-27579a214dc2a918e67bffb51a0825005e8bd42e.tar.gz rust-27579a214dc2a918e67bffb51a0825005e8bd42e.zip | |
Auto merge of #102573 - RalfJung:mirisync, r=oli-obk
Miri sync This is a Miri sync created with my experimental fork of josh. We should probably not merge this yet, but we can use this to check if the sync looks the way it should. r? `@oli-obk`
Diffstat (limited to 'src/ci/scripts/should-skip-this.sh')
| -rwxr-xr-x | src/ci/scripts/should-skip-this.sh | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/ci/scripts/should-skip-this.sh b/src/ci/scripts/should-skip-this.sh index c863f1b68c7..67ff00cc1df 100755 --- a/src/ci/scripts/should-skip-this.sh +++ b/src/ci/scripts/should-skip-this.sh @@ -18,10 +18,11 @@ if [[ -n "${CI_ONLY_WHEN_SUBMODULES_CHANGED-}" ]]; then # Submodules pseudo-files inside git have the 160000 permissions, so when # those files are present in the diff a submodule was updated. echo "Submodules were updated" - elif ! git diff --quiet "$BASE_COMMIT" -- src/tools/clippy src/tools/rustfmt; then + elif ! (git diff --quiet "$BASE_COMMIT" -- \ + src/tools/clippy src/tools/rustfmt src/tools/miri); then # There is not an easy blanket search for subtrees. For now, manually list # the subtrees. - echo "Clippy or rustfmt subtrees were updated" + echo "Tool subtrees were updated" elif ! (git diff --quiet "$BASE_COMMIT" -- \ src/test/rustdoc-gui \ src/librustdoc \ |