| commit | 461b8254d0054c6d5ae51a22d0706af80b1ca52e | [log] [tgz] |
|---|---|---|
| author | Dave Rodgman <dave.rodgman@arm.com> | Mon Jan 16 15:21:24 2023 +0000 |
| committer | GitHub <noreply@github.com> | Mon Jan 16 15:21:24 2023 +0000 |
| tree | 83fd86923e49fdf000eddf84ab56ef5c4b20a2f1 | |
| parent | 74d6e59e152dda5d4b5e85d2b9efca83ad32619c [diff] | |
| parent | 66edfe45f574e4db123d3a4dafb1d0cf6ac774d9 [diff] |
Merge pull request #6865 from scop/patch-1 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