aboutsummaryrefslogtreecommitdiffhomepage
path: root/html
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2003-09-24 23:37:05 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2003-09-24 23:37:05 +0000
commit00dfe954a92fb68601a72f0453d88f4af14a40c7 (patch)
tree5d482ade34e7b232e80b279e0dfce0fd44d9798e /html
parentccf89d821d14ee75e0917f9e579f7a4f4958ecb7 (diff)
Updated.
Diffstat (limited to 'html')
-rw-r--r--html/Kit/Makefile17
1 files changed, 11 insertions, 6 deletions
diff --git a/html/Kit/Makefile b/html/Kit/Makefile
index b35b720b..3a4e7591 100644
--- a/html/Kit/Makefile
+++ b/html/Kit/Makefile
@@ -1,11 +1,16 @@
#
-# Update dtds from PG Kit repository.
+# Update exported Kit files from PG Kit repository.
+# [interim]
#
-.PHONY: dtdupdate
+.PHONY: update
-DTDTARGS=dtd/pgip.dtd dtd/pgml.dtd
+CVSROOT=:pserver:da@cvs.inf.ed.ac.uk:/disk/cvs/proofgen
-# checkout in temp dir because otherwise CVS complains of repo clash (fixes?)
-dtdupdate:
- mkdir dtdtmp; cvs -d :ext:da@localssh.dcs.ed.ac.uk:/home/proofgen/src export -kv -D today -d dtdtmp Kit/dtd; mv dtdtmp/* dtd; rmdir dtdtmp; cvs commit -m"Updated from Kit repo" dtd
+# 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"