#! /bin/sh
# $Id$

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