On Nov 17, 12:17am, Jun T. wrote: } } The following (unessential) part has escaped from the commit: Thanks, I had a lot of trouble with that file for some reason (the patch kept failing to apply). Pushed now.