Updated maintenance scripts

So that they work with latest Gnome Terminal

diff --git a/tools/commit and push b/tools/commit and push
index 057b511..d659072 100755 (executable)
--- a/tools/commit and push
+++ b/tools/commit and push
@@ -1,10 +1,11 @@
 #!/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 ..
-
-cola
-git push
+(
+    cd ..
+    cola
+    git push
+)
 
 echo ""
 echo "Press ENTER to close this window."

diff --git a/tools/update web site b/tools/update web site
index ed2bf31..e8ccc71 100755 (executable)
--- a/tools/update web site
+++ b/tools/update web site
@@ -1,9 +1,10 @@
 #!/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 ..
-
-rsync -avz --delete  -e 'ssh -p 10006' doc/ n0@www3.svjatoslav.eu:/mnt/big/projects/javainspect/
+(
+    cd ..
+    rsync -avz --delete  -e 'ssh -p 10006' doc/ n0@www3.svjatoslav.eu:/mnt/big/projects/javainspect/
+)
 
 echo ""
 echo "Press ENTER to close this window."