Various updates to publish script
authorAryeh Gregor <AryehGregor+gitcommit@gmail.com>
Wed, 28 Sep 2011 15:07:52 -0600
changeset 629 0ae870dd03cd
parent 628 20505f74e222
child 630 197e383926ac
Various updates to publish script

No one else has reason to care about this.
publish
--- a/publish	Tue Sep 27 13:15:49 2011 -0600
+++ b/publish	Wed Sep 28 15:07:52 2011 -0600
@@ -2,13 +2,14 @@
 # This is the script I use on my server to publish the spec.  It's not really
 # useful for anyone else, I just want it in version control somewhere.
 set -e
-cd ~/webroot/spec/editing
-git pull
+cd ~/git/editing
+git fetch
 git push github
 cd ~/webroot/tmp/editing
 git fetch --all
-cd ~/webroot/spec
-rm -rf hg-editing || true
-hg clone ~/webroot/tmp/editing hg-editing
-cd hg-editing
+cd /tmp
+hg clone ~/webroot/tmp/editing hg-editing.$$
+cd hg-editing.$$
 hg push -r master https://dvcs.w3.org/hg/editing
+cd ..
+rm -rf hg-editing.$$