diff --git a/githooks/pre-push b/githooks/pre-push index 22f2a369..0972a764 100755 --- a/githooks/pre-push +++ b/githooks/pre-push @@ -1,5 +1,7 @@ #!/bin/bash +set -e + ROOT=`realpath $(dirname $0)/../..` pushd $ROOT make