aboutsummaryrefslogtreecommitdiffhomepage
path: root/html
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2001-09-13 16:04:59 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2001-09-13 16:04:59 +0000
commit13980845b34fb3c91b97cf06c3fac293bed56c33 (patch)
treea8c9d16df593986e40772095e7057b9b44d28c88 /html
parent6788e5d1d121ebbd54fe38842c56164bbeb100ad (diff)
New files.
Diffstat (limited to 'html')
-rw-r--r--html/Kit/Makefile11
1 files changed, 11 insertions, 0 deletions
diff --git a/html/Kit/Makefile b/html/Kit/Makefile
new file mode 100644
index 00000000..b35b720b
--- /dev/null
+++ b/html/Kit/Makefile
@@ -0,0 +1,11 @@
+#
+# Update dtds from PG Kit repository.
+#
+
+.PHONY: dtdupdate
+
+DTDTARGS=dtd/pgip.dtd dtd/pgml.dtd
+
+# 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