Today's github tip - fixing local master

[Dicebot]

On Wednesday, 19 June 2013 at 10:26:55 UTC, Jacob Carlborg wrote:
> On 2013-06-19 00:35, Walter Bright wrote:
>
>> No, the procedure is never push to upstream, do P.R.'s.
>
> Then wait for someone to merge the pull request. I don't 
> understand what you did and what you actually tried to do.

This. I am afraid wrong lesson was learned here. It is a 
dangerous signal that such working copy setup existed at all, not 
knowing how to fix it is a relatively minor problem.