Don't use bashism in checktools.sh
This commit is contained in:
parent
11f32b73e0
commit
14dda5fdfb
1 changed files with 1 additions and 1 deletions
|
@ -30,7 +30,7 @@ python3 "$X_PY" test --stage 2 src/tools/rustfmt
|
||||||
# We set the GC interval to the shortest possible value (0 would be off) to increase the chance
|
# We set the GC interval to the shortest possible value (0 would be off) to increase the chance
|
||||||
# that bugs which only surface when the GC runs at a specific time are more likely to cause CI to fail.
|
# that bugs which only surface when the GC runs at a specific time are more likely to cause CI to fail.
|
||||||
# This significantly increases the runtime of our test suite, or we'd do this in PR CI too.
|
# This significantly increases the runtime of our test suite, or we'd do this in PR CI too.
|
||||||
if [[ -z "${PR_CI_JOB:-}" ]]; then
|
if [ -z "${PR_CI_JOB:-}" ]; then
|
||||||
MIRIFLAGS=-Zmiri-provenance-gc=1 python3 "$X_PY" test --stage 2 src/tools/miri
|
MIRIFLAGS=-Zmiri-provenance-gc=1 python3 "$X_PY" test --stage 2 src/tools/miri
|
||||||
else
|
else
|
||||||
python3 "$X_PY" test --stage 2 src/tools/miri
|
python3 "$X_PY" test --stage 2 src/tools/miri
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue