<div dir="ltr">On 2020 December 19, I intend to merge !1196, (the first patch of) !1167, !1189, and !1137.<br><div><br></div><div>If there is a reason not to merge any of those feel compelled to comment now. This should also close #680, !957, and !1147.</div></div>