Update Makefile and add git pre-push hook (#1382)

2019-11-06 13:13:48 +08:00
parent 9272f0cb2c
commit 4b456db517
5 changed files with 41 additions and 28 deletions
@@ -0,0 +1,6 @@
+#!/bin/bash
+
+ROOT=`realpath $(dirname $0)/../..`
+pushd $ROOT
+make
+popd