egrep -> grep -E
The Makefile.coq.local
currently contains a check to ignore Coq 8.19 test output mismatches, introduced in !1011 (merged). This check uses egrep
:
COQ_NOREF=$(shell echo "$(COQ_VERSION)" | egrep "^8\.19[.+]" -q && echo 1)
egrep
has been obsolete for about 15 years now, it's simply an alias for grep -E
. To encourage users to switch from egrep
to grep -E
, newer versions of egrep
now annoy you to use grep -E
instead. See also this article. This leads to noisy build logs.
This PR fixes this.