diff options
author | 2003-09-24 23:37:05 +0000 | |
---|---|---|
committer | 2003-09-24 23:37:05 +0000 | |
commit | 00dfe954a92fb68601a72f0453d88f4af14a40c7 (patch) | |
tree | 5d482ade34e7b232e80b279e0dfce0fd44d9798e /html | |
parent | ccf89d821d14ee75e0917f9e579f7a4f4958ecb7 (diff) |
Updated.
Diffstat (limited to 'html')
-rw-r--r-- | html/Kit/Makefile | 17 |
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" |