On Saturday 05 May 2012 13:13:54 Paul Gardiner wrote: > I see. Ok. Thanks for the info. I guess github gets updated every now > and then, and so isn't wildly out of date for casual developers. One of our post-commit hooks syncs our repo with the copy on github. -- Stuart Morgan