1 files changed, 11 insertions, 0 deletions
diff --git a/tools/push b/tools/push
new file mode 100755
index 00000000..5bb95fb6
--- /dev/null
+++ b/tools/push
@@ -0,0 +1,11 @@
+#!/bin/sh
+
+git push origin
+git push --tags origin
+
+git push mirror
+git push --tags mirror
+
+git remote update
+
+github network fetch