#! /bin/sh
# $Id$
+configure="./configure"
+if [ "${1#*/configure}" != "$1" ];then
+ configure="$1"
+ shift
+fi
(
set -ex
rm -f config.cache
- export CFLAGS="-ggdb3"
- export CXXFLAGS="-ggdb3"
- ./configure --enable-static --disable-shared --disable-werror --enable-debug "$@"
+ flags="-ggdb2"
+ export CFLAGS="$flags"
+ export CXXFLAGS="$flags"
+ export GCJFLAGS="$flags"
+ time nice "$configure" --enable-static --disable-shared --enable-debug "$@"
) 2>&1|tee errs1