Re: Push is complete

[Bob Proulx]

Stefan Monnier wrote:
> > 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"?

Yes.  It requires more access.  In particular shell access.  But
several people have shell access no problem.  

I noticed that when I moved the 13G repository out of the way that a
cron task created an empty repository.  Then later I noticed that the
config file had been modified.  So I assume that there are multiple
people working on the task.  Which is fine.  But somewhere along the
way I am sure someone's edit will be lost.

Bob