| commit | 71d3ae09c1a2b045039cc11e857e597f68f1659f | [log] [tgz] |
|---|---|---|
| author | Dave Rodgman <dave.rodgman@arm.com> | Mon Jan 16 15:21:37 2023 +0000 |
| committer | GitHub <noreply@github.com> | Mon Jan 16 15:21:37 2023 +0000 |
| tree | fa042f90075bc2049a8f0f0b8b82209540a89114 | |
| parent | 4afd4b9be5ea1801bba9cac5e890c8d918bb5c0e [diff] | |
| parent | a74468155db9dc20d33b327df85f53241110dbde [diff] |
Merge pull request #6936 from daverodgman/patch-1-2.28 Use `grep -E` instead of `egrep`
diff --git a/tests/scripts/doxygen.sh b/tests/scripts/doxygen.sh index 2c523ba..e355073 100755 --- a/tests/scripts/doxygen.sh +++ b/tests/scripts/doxygen.sh
@@ -35,7 +35,7 @@ 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