diff options
| author | Dylan DPC <99973273+Dylan-DPC@users.noreply.github.com> | 2022-10-07 22:05:32 +0530 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-10-07 22:05:32 +0530 |
| commit | 3800d40dc8ca3d4bb9967cbee27d2c2bb7c12be6 (patch) | |
| tree | eace7c61d0cb06ecca5593f495fadc44c43448cb | |
| parent | d70e56aef8aa63e823009ed81b4acaf21e628b0f (diff) | |
| parent | 3d93c3848a4fa85487f930f93deb687d155761d6 (diff) | |
| download | rust-3800d40dc8ca3d4bb9967cbee27d2c2bb7c12be6.tar.gz rust-3800d40dc8ca3d4bb9967cbee27d2c2bb7c12be6.zip | |
Rollup merge of #102780 - RalfJung:miri-lib-sys, r=Mark-Simulacrum
run Miri CI when std::sys changes r? `@Mark-Simulacrum`
| -rwxr-xr-x | src/ci/scripts/should-skip-this.sh | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/ci/scripts/should-skip-this.sh b/src/ci/scripts/should-skip-this.sh index 67ff00cc1df..60c2960b160 100755 --- a/src/ci/scripts/should-skip-this.sh +++ b/src/ci/scripts/should-skip-this.sh @@ -19,9 +19,12 @@ if [[ -n "${CI_ONLY_WHEN_SUBMODULES_CHANGED-}" ]]; then # 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 src/tools/miri); then + src/tools/clippy src/tools/rustfmt src/tools/miri + library/std/src/sys); then # There is not an easy blanket search for subtrees. For now, manually list # the subtrees. + # Also run this when the platform-specific parts of std change, in case + # that breaks Miri. echo "Tool subtrees were updated" elif ! (git diff --quiet "$BASE_COMMIT" -- \ src/test/rustdoc-gui \ |