diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2001-09-13 16:04:59 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2001-09-13 16:04:59 +0000 |
commit | 13980845b34fb3c91b97cf06c3fac293bed56c33 (patch) | |
tree | a8c9d16df593986e40772095e7057b9b44d28c88 /html | |
parent | 6788e5d1d121ebbd54fe38842c56164bbeb100ad (diff) |
New files.
Diffstat (limited to 'html')
-rw-r--r-- | html/Kit/Makefile | 11 |
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 |