diff options
| author | David Aspinall | 2004-02-07 19:31:13 +0000 |
|---|---|---|
| committer | David Aspinall | 2004-02-07 19:31:13 +0000 |
| commit | b9caaa8e4b66817dbc66d0e79b567b3285869fea (patch) | |
| tree | c5420dac1aa1afc28168867ca5cc9c610a46399e /html/Makefile | |
| parent | 87174e13a8aa064f6d00ef9248da9938ea4978f6 (diff) | |
Deleted file
Diffstat (limited to 'html/Makefile')
| -rw-r--r-- | html/Makefile | 37 |
1 files changed, 0 insertions, 37 deletions
diff --git a/html/Makefile b/html/Makefile deleted file mode 100644 index 182a7a17..00000000 --- a/html/Makefile +++ /dev/null @@ -1,37 +0,0 @@ -# -# Publish files to Informatics web server. -# -# Requires permissions in /group/project/proofgeneral -# -# $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,.cvsignore - -# Run rsync using ssh -# --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 --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 - -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} - |