simplified website rsync

--- a/Admin/isasync	Fri Nov 23 21:09:35 2007 +0100
+++ b/Admin/isasync	Mon Nov 26 10:42:39 2007 +0100
@@ -17,7 +17,7 @@
   echo "  Options are:"
   echo "    -h    print help message"
   echo "    -n    dry run, don't do anything, just report what would happen"
-  echo "    -w    mirror whole Isabelle website"
+  echo "    -w    (ignored for backward compatibility)"
   echo "    -d    delete files that are not on the server (BEWARE!)"
   echo
   exit 1
@@ -36,7 +36,7 @@
 
 HELP=""
 ARGS=""
-SRC="isabelle-distribution"
+SRC="isabelle-website"
 
 while getopts "hnwd" OPT
 do
@@ -48,7 +48,7 @@
       ARGS="$ARGS -n"
       ;;
     w)
-      SRC="isabelle-website"
+      echo "option -w ignored"
       ;;
     d)
       ARGS="$ARGS --delete"

--- a/Admin/mirror-website	Fri Nov 23 21:09:35 2007 +0100
+++ b/Admin/mirror-website	Mon Nov 26 10:42:39 2007 +0100
@@ -10,7 +10,7 @@
   sunbroy2)
     DEST=/home/html/isabelle/html-data
     ;;
-  atbroy1)
+  atbroy*)
     DEST=/home/html/isabelle/html-data
     ;;
   *.cl.cam.ac.uk)
@@ -23,4 +23,4 @@
     ;;
 esac
 
-exec $(dirname $0)/isasync -w $DEST
+exec $(dirname $0)/isasync $DEST