diff options
Diffstat (limited to 'html/Kit/Makefile')
| -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 |