tools/update web site

   1 #!/bin/bash
   2 cd "${0%/*}"; if [ "$1" != "T" ]; then gnome-terminal -- "$0" T; exit; fi
   3
   4 (
   5     cd ..
   6     rsync -avz --delete  -e 'ssh -p 10006' doc/ n0@www3.svjatoslav.eu:/mnt/big/projects/javainspect/
   7 )
   8
   9 echo ""
  10 echo "Press ENTER to close this window."
  11 read