Merge pull request #148 from oscarbenjamin/pr_no_debug

Disable debug symbols in Flint build
flintlib · Jun 19, 2024 · 82b8511 · 82b8511
2 parents 33a4daa + 636e19d
commit 82b8511
Showing 1 changed file with 2 additions and 1 deletion.
diff --git 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 ..