On 2018-04-23 19:25, Joshua Root wrote:
On 2018-4-24 03:19 , Ken Cunningham wrote:Revert? No many would have the accidental update....The commit was never on master, so there's no problem.
Yes, I usually work on a branch exactly to protect against pushing to the wrong repo by accident. That day came today. I deleted the branch moments after pushing.
I'm almost finished with the revbump of dependant ports, will create a PR within the hour.
// Leonardo.