# HG changeset patch
# User haftmann
# Date 1196070159 -3600
# Node ID 8b9c4582795aab27b208411d6bc6cf326c883b29
# Parent  dad0291cb76aba4e758ff0eb53902ba88e01cae1
simplified website rsync

diff -r dad0291cb76a -r 8b9c4582795a Admin/isasync
--- 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"
diff -r dad0291cb76a -r 8b9c4582795a Admin/mirror-website
--- 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