diff options
-rw-r--r-- | src/Makefile.am | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index d9e89108d..99892734b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -139,7 +139,7 @@ check-exported-symbols: $(LTLIBRARIES) if [ -f "$(LIBMPFRSO)" ]; then \ gsymbols=`$(NM) -gP "$(LIBMPFRSO)" | perl -ne \ '/^(__gmp[a-z]?_[_0-9A-Za-z]*) +[A-TV-Z]/ and print " $$1"' | \ - grep -v '@plt$$'`; \ + { grep -v '@plt$$' || true ; }`; \ if [ -n "$$gsymbols" ]; then \ echo "MPFR defines symbols with a GMP reserved prefix:$$gsymbols"; \ exit 1; \ |