Merge pull request #6936 from daverodgman/patch-1-2.28

Use `grep -E` instead of `egrep`
Mbed-TLS · Jan 16, 2023 · 71d3ae0 · 71d3ae0
2 parents 4afd4b9 + a744681
commit 71d3ae0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tests/scripts/doxygen.sh b/tests/scripts/doxygen.sh
@@ -35,7 +35,7 @@ cat doc.out doc.err | \
     grep -v "warning: ignoring unsupported tag" \
     > doc.filtered
 
-if egrep "(warning|error):" doc.filtered; then
+if grep -E "(warning|error):" doc.filtered; then
     echo "FAIL" >&2
     exit 1;
 fi