diff --git a/Misc/build.sh b/Misc/build.sh index 782fe591443..ecbe57970fd 100755 --- a/Misc/build.sh +++ b/Misc/build.sh @@ -273,8 +273,9 @@ echo "" >> $RESULT_FILE echo "" >> $RESULT_FILE ## copy results -chgrp -R webmaster build/html -chmod -R g+w build/html -rsync $RSYNC_OPTS build/html/* $REMOTE_SYSTEM:$REMOTE_DIR -cd ../build -rsync $RSYNC_OPTS index.html *.out $REMOTE_SYSTEM:$REMOTE_DIR/results/ +## (not used anymore, the daily build is now done directly on the server) +#chgrp -R webmaster build/html +#chmod -R g+w build/html +#rsync $RSYNC_OPTS build/html/* $REMOTE_SYSTEM:$REMOTE_DIR +#cd ../build +#rsync $RSYNC_OPTS index.html *.out $REMOTE_SYSTEM:$REMOTE_DIR/results/