From 636e19d558e51472a6b150230399e792f55fd547 Mon Sep 17 00:00:00 2001 From: Oscar Benjamin Date: Wed, 19 Jun 2024 23:00:41 +0100 Subject: [PATCH] Disable debug symbols in Flint build --- bin/build_dependencies_unix.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/bin/build_dependencies_unix.sh b/bin/build_dependencies_unix.sh index 7f807a9f..2324b10d 100755 --- a/bin/build_dependencies_unix.sh +++ b/bin/build_dependencies_unix.sh @@ -284,7 +284,8 @@ cd flint-$FLINTVER ./configure --prefix=$PREFIX\ $FLINTARB_WITHGMP\ --with-mpfr=$PREFIX\ - --disable-static + --disable-static\ + --disable-debug make -j6 make install cd ..