also pull before push to git

[physical.git] / repository handling tools / commit and push

diff --git a/repository handling tools/commit and push b/repository handling tools/commit and push
index 057b511..a2bafd7 100755 (executable)
--- a/repository handling tools/commit and push
+++ b/repository handling tools/commit and push
@@ -1,9 +1,12 @@
 #!/bin/bash
-cd "${0%/*}"; if [ "$1" != "T" ]; then gnome-terminal -e "'$0' T"; exit; fi;
+
+cd "${0%/*}"; if [ "$1" != "T" ]; then gnome-terminal -- "$0" T; exit; fi;
 
 cd ..
 
+git add --all
 cola
+git pull
 git push
 
 echo ""