Skip to content

Commit 82b8511

Browse files
Merge pull request #148 from oscarbenjamin/pr_no_debug
Disable debug symbols in Flint build
2 parents 33a4daa + 636e19d commit 82b8511

File tree

1 file changed

+2
-1
lines changed

1 file changed

+2
-1
lines changed

bin/build_dependencies_unix.sh

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -284,7 +284,8 @@ cd flint-$FLINTVER
284284
./configure --prefix=$PREFIX\
285285
$FLINTARB_WITHGMP\
286286
--with-mpfr=$PREFIX\
287-
--disable-static
287+
--disable-static\
288+
--disable-debug
288289
make -j6
289290
make install
290291
cd ..

0 commit comments

Comments
 (0)