diff options
| author | Ralf Jung <post@ralfj.de> | 2022-10-07 14:39:07 +0200 |
|---|---|---|
| committer | Ralf Jung <post@ralfj.de> | 2022-10-07 14:39:07 +0200 |
| commit | 3d93c3848a4fa85487f930f93deb687d155761d6 (patch) | |
| tree | ba44c3f5e7bd1a07e61efa4728385ac6e4677195 | |
| parent | 58546803885164d488185fb9cb9fb04fcbe64e30 (diff) | |
| download | rust-3d93c3848a4fa85487f930f93deb687d155761d6.tar.gz rust-3d93c3848a4fa85487f930f93deb687d155761d6.zip | |
run Miri CI when std::sys changes
| -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 \ |