No longer need this script.

2020-01-31 09:25:51 +02:00 · 2020-01-31 09:25:51 +02:00 · 4b7edf491b
parent 93fb90153f
commit 4b7edf491b
1 changed files with 0 additions and 4 deletions
--- a/scripts/pushtogit.sh
+++ b/scripts/pushtogit.sh
@ -1,4 +0,0 @@
-#!/bin/sh
-
-hg bookmark -f master;
-hg push -f github