diff options
| -rwxr-xr-x | Misc/build.sh | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/Misc/build.sh b/Misc/build.sh index 81cc647..5d096ee 100755 --- a/Misc/build.sh +++ b/Misc/build.sh @@ -284,9 +284,10 @@ echo "</body>" >> $RESULT_FILE echo "</html>" >> $RESULT_FILE ## copy results -chgrp -R webmaster build/html -chmod -R g+w build/html -rsync $RSYNC_OPTS build/html/* $REMOTE_SYSTEM:$REMOTE_DIR -rsync $RSYNC_OPTS dist/* $REMOTE_SYSTEM:$REMOTE_DIR_DIST -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 +#rsync $RSYNC_OPTS dist/* $REMOTE_SYSTEM:$REMOTE_DIR_DIST +#cd ../build +#rsync $RSYNC_OPTS index.html *.out $REMOTE_SYSTEM:$REMOTE_DIR/results/ |