On 01/03/2017 07:49 PM, Bruce Momjian wrote:
> On Tue, Jan 3, 2017 at 06:46:32PM +0100, Magnus Hagander wrote:
>> Is this a big enough boo that we actually want to reset the master repo to get
>> rid of it?
>>
>> If so, we need to do it *now* beore people get a chance to mirror it properly..
>>
>> Thoughts?
>>
>> If not, just a revert should work of course..
>
> OK, not sure how this happened but I think it has to do with my
> accidentally doing a 'pull' after the changes, and doing multiple
> branches.
>
> Whatever you suggest is fine --- I will wait.
I'm leaning for +1 for resetting. It'll be a pain for any mirrors of the
repo, but I think the clean history is worth it.
- Heikki
