Allow setting EXTRA_FLAGS_RELEASE to something other than -O0.

(cherry-picked from commit 2ed9d2c0c4)
This commit is contained in:
pentarctagon 2018-04-14 01:10:02 -05:00 committed by Jyrki Vesterinen
parent 4bb16f25a7
commit a07b847181

View file

@ -2,7 +2,7 @@
date
export EXTRA_FLAGS_RELEASE=""
export EXTRA_FLAGS_RELEASE="$OPT"
export WML_TESTS=true
export PLAY_TEST=true
export MP_TEST=true
@ -10,7 +10,6 @@ export WML_TEST_TIME=15
export BOOST_TEST=true
if [ "$OPT" = "-O0" ]; then
export EXTRA_FLAGS_RELEASE="-O0"
export PLAY_TEST=false
export MP_TEST=false
export WML_TEST_TIME=20