Auto merge of #2544 - saethlin:egrep, r=saethlin
Don't use egrep, we don't need it As of a few days ago, the latest version of `egrep` is now this: ```sh #!/bin/sh cmd=${0##*/} echo "$cmd: warning: $cmd is obsolescent; using grep -E" >&2 exec grep -E "$`@"` ``` Fortunately we don't actually need ERE, so we can just drop the e.
This commit is contained in:
commit
bb3bac0373
@ -33,7 +33,7 @@ echo "$NEW_COMMIT" > rust-version
|
||||
shift || true # don't fail if shifting fails
|
||||
|
||||
# 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
|
||||
echo "miri toolchain is already at commit $CUR_COMMIT."
|
||||
rustup override set miri
|
||||
|
Loading…
Reference in New Issue
Block a user