Re: Push is complete

[Stefan Monnier]

> It also looks like there are multiple people (and possibly automated
> processes) editing the git config file.  It would be good if anyone
> who is editing that file would be so kind as to drop me a note to
> coordinate.  Otherwise when I re-enable things subsequent edits will
> surely be lost there.

FWIW, I don't even know how to modify this file.  Doesn't it require
more access rights than just "write access to the repository"?


        Stefan