Kevin Grittner wrote:
> 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.
FWIW this email was stuck in the moderation queue, I just released it.
We might have realized earlier that there was a problem ...
--
Álvaro Herrera http://www.2ndQuadrant.com/
PostgreSQL Development, 24x7 Support, Training & Services