diff options
| author | David Aspinall | 2003-11-07 14:14:35 +0000 |
|---|---|---|
| committer | David Aspinall | 2003-11-07 14:14:35 +0000 |
| commit | 1a3429a036ef1ecfbb4cc11d2f28e52e03f94a97 (patch) | |
| tree | 8bc7995f55f3471a616431f5e6a65466ab12b290 /html | |
| parent | 4183a528bbc5b1e94205ce987511d3cfd2b3fb47 (diff) | |
FIXME
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 |