| 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`