diff options
Diffstat (limited to 'html')
| -rw-r--r-- | html/Makefile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/html/Makefile b/html/Makefile index 54aca8ff..182a7a17 100644 --- a/html/Makefile +++ b/html/Makefile @@ -17,7 +17,7 @@ IGNOREDWEBFILES=*~,*.NOEXPORT,CVS/,/test/,/test/*,/tmp,/tmp/*,/Makefile,.cvsigno # --include=ProofGeneral-* to avoid deleting archives # --delete-excluded EXCLUDEFILE=.tmp-rsync-excludes -RSYNC=rsync -e ssh -auv --safe-links --force --exclude-from=${EXCLUDEFILE} --include='ProofGeneral-*' --exclude="/${EXCLUDEFILE}" --cvs-exclude +RSYNC=rsync -e ssh -auv --safe-links --force --exclude-from=${EXCLUDEFILE} --include='releases-emacs' --exclude="/${EXCLUDEFILE}" --cvs-exclude DESTWEB=ssh.inf.ed.ac.uk:/group/project/proofgeneral/web DESTCGI=ssh.inf.ed.ac.uk:/group/project/proofgeneral/cgi |