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

2019-11-08 23:47:40 +08:00
parent 8176160802
commit c2ec855909
1 changed files with 2 additions and 0 deletions
@@ -1,5 +1,7 @@
 #!/bin/bash

+set -e
+
 ROOT=`realpath $(dirname $0)/../..`
 pushd $ROOT
 make