#! /bin/sh
# $Id$

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