[tools/mpfrlint] Correction for zsh change after v5.2 (POSIX compat:

"set -e; f() { false && true; }; f; echo OK" no longer prints OK).

git-svn-id: svn://scm.gforge.inria.fr/svn/mpfr/trunk@10969 280ebfd0-de03-0410-8827-d642c229c3f4

1 files changed, 2 insertions, 0 deletions

diff --git a/tools/mpfrlint b/tools/mpfrlint
index f4e0eb6cd..53293f896 100755
--- a/tools/mpfrlint
+++ b/tools/mpfrlint
@@ -61,6 +61,8 @@ err-if-output()
   fi
   set -e
   [[ -n $dir ]] && popd
+  # Do not fail.
+  true
 }
 
 if [[ $1 == test ]] then