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/Kit/Makefile | 16 ----------------
 1 file changed, 16 deletions(-)
 delete mode 100644 html/Kit/Makefile

(limited to 'html/Kit/Makefile')

diff --git a/html/Kit/Makefile b/html/Kit/Makefile
deleted file mode 100644
index 3a4e7591..00000000
--- a/html/Kit/Makefile
+++ /dev/null
@@ -1,16 +0,0 @@
-#
-# Update exported Kit files from PG Kit repository.
-# [interim]
-#
-
-.PHONY: update
-
-CVSROOT=:pserver:da@cvs.inf.ed.ac.uk:/disk/cvs/proofgen
-
-# checkout in temp dir because otherwise CVS complains of working dir checkout
-update:	
-	mkdir kittmp
-	cvs -d ${CVSROOT} export -kv -D today -d kittmp kitwebfiles
-	(cd kittmp; tar -c . | (cd ..; tar -xp))
-	rm -rf kittmp
-	cvs commit -m"Updated from Kit repo"
-- 
cgit v1.2.3