3 #OPTIONS="--disable-optimization --enable-debug"
6 #OPTIONS="$OPTIONS --enable-timelimit=120"
7 OPTIONS="$OPTIONS --enable-optimization=2"
8 OPTIONS="$OPTIONS --enable-optimization=3 --enable-g5opt"
9 #OPTIONS="$OPTIONS --disable-optimization"
10 OPTIONS="$OPTIONS --disable-debug"
14 [ -e configure ] || ./bootstrap || exit 1
16 [ -d $BUILDDIR ] && rm -fr $BUILDDIR
22 ../configure $OPTIONS || exit 1