Fix githook not aborting push if error occurrs (#1386)

2019-11-08 23:47:40 +08:00
parent 19753e07e0
commit 6f5f6900b6
1 changed files with 2 additions and 0 deletions
@@ -1,5 +1,7 @@
 #!/bin/bash
 set -e
 ROOT=`realpath $(dirname $0)/../..`
 pushd $ROOT
 make