Alex Vandiver <a...@chmrr.net> writes:
> [remote "github"]
> url = g...@github.com:bestpractical/rt.git
> fetch = +refs/*:refs/*
> mirror = yes
"git push github master^:master" must stay a usable way to update
the published repository to an arbitrary commit, so "if set to
mirror, do not pretend that a fetch in reverse has happened during
'git push'" will not be a solution to this issue.
Perhaps removing remote.github.fetch would be one sane way forward.
Otherwise, even if your "git push" does not pretend to immediately
fetch from there (i.e. even if the reported behaviour was a bug,
without doing anything to trigger it) somebody running "git fetch"
in this repository can destroy what other person pushes into this
repository at the same time exactly the same way, I would think.
To unsubscribe from this list: send the line "unsubscribe git" in
the body of a message to majord...@vger.kernel.org
More majordomo info at http://vger.kernel.org/majordomo-info.html