#! /bin/sh
# $Id$

set -ex
test -n "$*"
trap 'git reset --hard;git clean -df;exit 125' EXIT
git reset --hard
git clean -df
errs12 -s --fast --disable-werror --without-python --disable-plugins
trap '' EXIT
set +e
"$@" 
rc=$?
set -e
#git reset --hard
#git clean -df
echo rc=$rc
exit $rc