diff options
| author | Ralf Jung <post@ralfj.de> | 2022-10-04 15:23:57 +0200 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2022-10-04 17:31:49 +0200 |
| commit | 9cc11e262f1c8313ec11154a2d5440ff5664aec4 (patch) | |
| tree | 89d76a9e3a632d2715db09e315d0a5b05776f299 /src/ci/scripts | |
| parent | 6f2b52ff103f9095fb2817637bc7d388bd4c7f6b (diff) | |
| download | rust-9cc11e262f1c8313ec11154a2d5440ff5664aec4.tar.gz rust-9cc11e262f1c8313ec11154a2d5440ff5664aec4.zip | |
test Miri changes in PR CI; we no longer need xargo
Diffstat (limited to 'src/ci/scripts')
| -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 \ |