+--origss

diff --git a/bin/errs1 b/bin/errs1
index 43d99b8..5637f9d 100755 (executable)
--- a/bin/errs1
+++ b/bin/errs1
@@ -6,6 +6,11 @@ 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
@@ -13,5 +18,5 @@ fi
        export CFLAGS="$flags"
        export CXXFLAGS="$flags"
        export GCJFLAGS="$flags"
-       time nice "$configure" --enable-static --disable-shared --enable-debug "$@"
+       time nice "$configure" $customss --enable-debug "$@"
        ) 2>&1|tee errs1