diff --git a/util/build-gnu.sh b/util/build-gnu.sh index d29283a69..b1daee7e6 100755 --- a/util/build-gnu.sh +++ b/util/build-gnu.sh @@ -122,6 +122,8 @@ if test -f gnu-built; then echo "'rm -f $(pwd)/gnu-built' to force the build" echo "Note: the customization of the tests will still happen" else + # Disable useless checks + sed -i 's|check-texinfo: $(syntax_checks)|check-texinfo:|' doc/local.mk ./bootstrap --skip-po ./configure --quiet --disable-gcc-warnings --disable-nls --disable-dependency-tracking --disable-bold-man-page-references #Add timeout to to protect against hangs