diff options
Diffstat (limited to '.ci')
| -rwxr-xr-x | .ci/verify_symbols.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.ci/verify_symbols.sh b/.ci/verify_symbols.sh index 2fe2d5d..73cc6ba 100755 --- a/.ci/verify_symbols.sh +++ b/.ci/verify_symbols.sh @@ -29,7 +29,7 @@ main() { local symbol for symbol; do - if echo "$nm" | grep -F --quiet -e " $symbol"; then + if echo "$nm" | grep -F -e " $symbol"; then echo "$script_name: file '$path' has symbol '$symbol'" else echo "$script_name: symbol '$symbol' wasn't found in file '$path'" |