diff options
Diffstat (limited to 'html')
| -rw-r--r-- | html/Makefile | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/html/Makefile b/html/Makefile index cf34a8ea..54aca8ff 100644 --- a/html/Makefile +++ b/html/Makefile @@ -5,14 +5,19 @@ # # $Id$ # +# FIXME: we want to have --delete and --delete-excluded in sync, +# but yet preserve ProofGeneral-* (distribs). How to do that? +# Might be better to put distribs elsewhere. PWD=`pwd` -IGNOREDWEBFILES="*~,*.NOEXPORT,CVS/,/test/,/test/*,/tmp,/tmp/*,/Makefile" +IGNOREDWEBFILES=*~,*.NOEXPORT,CVS/,/test/,/test/*,/tmp,/tmp/*,/Makefile,.cvsignore # Run rsync using ssh -# --cvs-exclude: auto ignore files in the same way CVS does [inc. .cvsignore] +# --cvs-exclude: auto ignore files in the same way CVS does [exc. .cvsignore] +# --include=ProofGeneral-* to avoid deleting archives +# --delete-excluded EXCLUDEFILE=.tmp-rsync-excludes -RSYNC=rsync -e ssh -auv --delete --safe-links --force --delete-excluded --exclude-from=${EXCLUDEFILE} --exclude="/${EXCLUDEFILE}" +RSYNC=rsync -e ssh -auv --safe-links --force --exclude-from=${EXCLUDEFILE} --include='ProofGeneral-*' --exclude="/${EXCLUDEFILE}" --cvs-exclude DESTWEB=ssh.inf.ed.ac.uk:/group/project/proofgeneral/web DESTCGI=ssh.inf.ed.ac.uk:/group/project/proofgeneral/cgi |