Kevin Grittner <kgrittn@ymail.com> wrote:
> Pushed.
My first attempt to push it failed because of a concurrent commit
by Tom, and then when I went to redo it I accidentally included a
file with the .orig suffix. I think I've undone my error, but
github doesn't seem to be updating, so I fear I did some damage
somehow. If someone who knows what they are doing with git better
than I do could check the server to make sure there is no residual
problem, I would appreciate it.
Sorry for the trouble.
--
Kevin Grittner
EnterpriseDB: http://www.enterprisedb.com
The Enterprise PostgreSQL Company