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