10 Sep
2018
10 Sep
'18
1:06 p.m.
Hi all, due to a mistaken merge yesterday evening EDT (about 15 hours ago), we've rewound the history to plop that one topmost commit off. We're currently waiting to see whether this causes nontrivial problems for anyone, so if you have any issues please send an e-mail or speak up on Slack. If it does cause issues, we'll re-push the ill-fated merge commit and do the revert on top of that. Apologies for any inconveniences caused, -David