diff options
| -rwxr-xr-x | tools/mpfrlint | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/tools/mpfrlint b/tools/mpfrlint index d717fb6d3..7d4c7093b 100755 --- a/tools/mpfrlint +++ b/tools/mpfrlint @@ -173,6 +173,12 @@ err-if-output --msg="Use GMP_NUMB_BITS instead." \ grep GMP_RND $srctests | err-if-output -t "GMP_RND*" grep -v '#define GMP_RND' +# __MPFR_DECLSPEC (based on the __MPFR_WITHIN_MPFR status) must be used +# instead of __GMP_DECLSPEC (based on the __GMP_WITHIN_GMP status, always +# undefined in MPFR). +err-if-output --msg="Use __MPFR_DECLSPEC instead." -t "__GMP_DECLSPEC" \ + grep --exclude=src/mpfr.h __GMP_DECLSPEC $srctests + # Use mpfr_div_2ui/mpfr_mul_2ui instead of mpfr_div_2exp/mpfr_mul_2exp. grep 'mpfr_\(div\|mul\)_2exp' {src,tests}/*.{c,h} |\ grep -v '^src/\(\(div\|mul\)_2exp\.c:\|mpf2mpfr\.h:#define mpf_\)' | \ |