diff options
| author | David Aspinall | 2003-11-07 12:49:49 +0000 |
|---|---|---|
| committer | David Aspinall | 2003-11-07 12:49:49 +0000 |
| commit | bba71a8ce80e33b4331f2b02a7a072086de08872 (patch) | |
| tree | 268ca3108e2b1ae5f0d8e5dffd68bc7748efe1b8 | |
| parent | 827ddd2b4923e0f3fdf245c8abd3e9ff4c4d3dcb (diff) | |
New files.
| -rw-r--r-- | html/Makefile | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/html/Makefile b/html/Makefile new file mode 100644 index 00000000..cf34a8ea --- /dev/null +++ b/html/Makefile @@ -0,0 +1,32 @@ +# +# Publish files to Informatics web server. +# +# Requires permissions in /group/project/proofgeneral +# +# $Id$ +# + +PWD=`pwd` +IGNOREDWEBFILES="*~,*.NOEXPORT,CVS/,/test/,/test/*,/tmp,/tmp/*,/Makefile" + +# Run rsync using ssh +# --cvs-exclude: auto ignore files in the same way CVS does [inc. .cvsignore] +EXCLUDEFILE=.tmp-rsync-excludes +RSYNC=rsync -e ssh -auv --delete --safe-links --force --delete-excluded --exclude-from=${EXCLUDEFILE} --exclude="/${EXCLUDEFILE}" + +DESTWEB=ssh.inf.ed.ac.uk:/group/project/proofgeneral/web +DESTCGI=ssh.inf.ed.ac.uk:/group/project/proofgeneral/cgi + +default: pub + +excludes: + echo '${IGNOREDWEBFILES}' | sed 's/,/\n/g' > ${EXCLUDEFILE} + +test: excludes + ${RSYNC} --exclude=/cgi/ -n ${PWD}/ ${DESTWEB} +# ${RSYNC} -n ${PWD}/cgi/ ${DESTCGI} + +pub: excludes + ${RSYNC} --exclude=/cgi/ ${PWD}/ ${DESTWEB} +# ${RSYNC} ${PWD}/cgi/ ${DESTCGI} + |