Skip to content

egrep -> grep -E

Johannes Hostert requested to merge johannes/iris:egrep into master

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.

Merge request reports