I’ve gone ahead and uploaded these changes. Since I don’t have access to the repository on repo.or.cz, I’ve pushed my commits to https://salsa.debian.org/andersk-guest/git debian-sid. Jonathan, you can mirror these to repo.or.cz at your convenience, or we can take this opportunity to set up a shared repository on salsa.
Anders
