Kevin Grittner <[email protected]> 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 -- Sent via pgsql-committers mailing list ([email protected]) To make changes to your subscription: http://www.postgresql.org/mailpref/pgsql-committers
