diff options
| -rwxr-xr-x | tools/build-patch | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tools/build-patch b/tools/build-patch index e47564ae6..3780e3bfc 100755 --- a/tools/build-patch +++ b/tools/build-patch @@ -78,6 +78,11 @@ if [[ $# -ge 1 ]] then echo $3 >> PATCHES fi fi + if ! cmp --quiet $mpfrdir/$base-{a,b}/doc/mpfr.texi; then + ./configure + make info + make distclean + fi popd set +e TZ=UTC diff -Naurd $base-a $base-b > $newpatch |