--- a/Admin/isasync Sat Nov 19 14:22:28 2005 +0100
+++ b/Admin/isasync Mon Nov 21 10:44:14 2005 +0100
@@ -128,4 +128,4 @@
## main
-exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC/." "$DEST/."
+exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC" "$DEST/"
--- a/Admin/website/README Sat Nov 19 14:22:28 2005 +0100
+++ b/Admin/website/README Mon Nov 21 10:44:14 2005 +0100
@@ -117,7 +117,7 @@
* do "make perms" to set file owner group (isabelle) and permissions
(rw-rw-r--, rwxrwsr-x)
* do your changes
-* just type make - the website is builded to the website synchronization cache
+* just type make - the website is built to the website synchronization cache
* then do CVS commit
* for updating the webpage in Munich, just use Admin/mirror-website
* if the Isabelle distribution files themselves change, some handwired updating
--- a/Admin/website/TODO Sat Nov 19 14:22:28 2005 +0100
+++ b/Admin/website/TODO Mon Nov 21 10:44:14 2005 +0100
@@ -1,9 +1,3 @@
-For the release:
-- announce build bed
-- abandon old scripts: mirror-*, rsyncisabelle
-- abandon old cache
-- cleanup website mess
-
In the mid-time:
- a gentle intro enumeration on Home - "Why Isabelle?"
* stably running, mature system
--- a/Admin/website/build/project.mak Sat Nov 19 14:22:28 2005 +0100
+++ b/Admin/website/build/project.mak Mon Nov 21 10:44:14 2005 +0100
@@ -20,21 +20,21 @@
mkdir -p $@
$(COPY) -vRud $</[^w]* $@
-chgrp -hR $(TARGET_GROUP) $@
- -chmod -R u-w,g-w,o-w $@
- -[ ! -e Isabelle ] && ln -s $(ISABELLE_DIST)/$(DISTNAME) $@/Isabelle
+ -chmod -R u+w,g-w,o-w $@
+ -[ ! -e $@/Isabelle ] && ln -s $(ISABELLE_DIST)/$(DISTNAME) $@/Isabelle
-chgrp -h $(TARGET_GROUP) $@/Isabelle
- -chmod u-w,g-w,o-w $@/Isabelle
+ -chmod u+w,g-w,o-w $@/Isabelle
else
$(OUTPUTROOT)/dist: $(ISABELLE_DIST) SYNC_ALWAYS
mkdir -p $@
- $(RSYNC) -v --exclude='/website/' -rltgoD --delete --delete-after $</ $@
+ $(RSYNC) -v --exclude='/website/' -rlt --delete --delete-after $</ $@
-chgrp -hR $(TARGET_GROUP) $@
- -chmod -R u-w,g-w,o-w $@
- -[ ! -e Isabelle ] && ln -s $(ISABELLE_DIST)/$(DISTNAME) $@/Isabelle
+ -chmod -R u+w,g-w,o-w $@
+ -[ ! -e $@/Isabelle ] && ln -s $(ISABELLE_DIST)/$(DISTNAME) $@/Isabelle
-chgrp -h $(TARGET_GROUP) $@/Isabelle
- -chmod u-w,g-w,o-w $@/Isabelle
+ -chmod u+w,g-w,o-w $@/Isabelle
SYNC_ALWAYS: