diff options
Diffstat (limited to 'tools/push')
-rwxr-xr-x | tools/push | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/tools/push b/tools/push deleted file mode 100755 index 926f1661..00000000 --- a/tools/push +++ /dev/null @@ -1,11 +0,0 @@ -#!/bin/sh - -git push origin -git push --tags origin - -git push mirror -git push --tags mirror - -git remote update - -#github network fetch |