On 08/05/2014 05:38 AM, Joseph S. Myers wrote: > It looks like you committed the ChangeLog entry but not the actual > removal.... Bah. Dunno how I flubbed that. Pushed the real delete now. r~