Thanks, I've merged your branch now. The only changes I made were to fix up some tab/space desynchronisation in update-grub and to add a debian/changelog entry.
Thanks, I've merged your branch now. The only changes I made were to fix up some tab/space desynchronisation in update-grub and to add a debian/changelog entry.