From d445edfd196e79e40b07bfc093d05bc79f5f4645 Mon Sep 17 00:00:00 2001 From: Sylvestre Ledru Date: Mon, 13 Jan 2025 10:15:33 +0100 Subject: [PATCH] GNU build: disable an old check --- util/build-gnu.sh | 2 ++ 1 file changed, 2 insertions(+) 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