Unfortunately, the Github interface does no longer allow me to edit a file in the GUI and then branch it in my personal clone for making a PR. It now only offers to make a PR using a branch on the ansible repository :-(
So committing this directly instead against my will, but per the guidelines this appears to be safe. Fingers crossed...