| changeset 17948 | 58ddfa89e6c0 |
| parent 17947 | d878a7735ff6 |
| child 17949 | 0150d6d7728b |
--- a/Admin/website/build/project.mak Fri Oct 21 10:27:02 2005 +0200 +++ b/Admin/website/build/project.mak Fri Oct 21 10:32:04 2005 +0200 @@ -29,7 +29,7 @@ $(OUTPUTROOT)/dist: $(ISABELLE_DIST) SYNC_ALWAYS mkdir -p $@ - $(RSYNC) -v --exclude='/website/' -a --delete --delete-after $</ $@ + $(RSYNC) -v --exclude='/website/' -rltgoD --delete --delete-after $</ $@ chgrp -hR $(TARGET_GROUP) $@ chmod -R u-w,g-w,o-w $@ -[ ! -e Isabelle ] && ln -s $(ISABELLE_DIST)/$(DISTNAME) $@/Isabelle