don't use egrep, we don't need it
This commit is contained in:
parent
2f1fa12659
commit
a094296e8b
1 changed files with 1 additions and 1 deletions
|
@ -33,7 +33,7 @@ echo "$NEW_COMMIT" > rust-version
|
||||||
shift || true # don't fail if shifting fails
|
shift || true # don't fail if shifting fails
|
||||||
|
|
||||||
# Check if we already are at that commit.
|
# Check if we already are at that commit.
|
||||||
CUR_COMMIT=$(rustc +miri --version -v 2>/dev/null | egrep "^commit-hash: " | cut -d " " -f 2)
|
CUR_COMMIT=$(rustc +miri --version -v 2>/dev/null | grep "^commit-hash: " | cut -d " " -f 2)
|
||||||
if [[ "$CUR_COMMIT" == "$NEW_COMMIT" ]]; then
|
if [[ "$CUR_COMMIT" == "$NEW_COMMIT" ]]; then
|
||||||
echo "miri toolchain is already at commit $CUR_COMMIT."
|
echo "miri toolchain is already at commit $CUR_COMMIT."
|
||||||
rustup override set miri
|
rustup override set miri
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue