From b9caaa8e4b66817dbc66d0e79b567b3285869fea Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 7 Feb 2004 19:31:13 +0000
Subject: Deleted file

---
 html/Makefile | 37 -------------------------------------
 1 file changed, 37 deletions(-)
 delete mode 100644 html/Makefile

(limited to 'html/Makefile')

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}
-
-- 
cgit v1.2.3