Thanks Paul and Eli.

> Yes. And you're welcome to do it. We're better off if more people know how to do it. Please see admin/notes/git-workflow. It needs updating (at least to change "emacs-24" to "emacs-25"), and you can do that before merging....

Would someone kindly do that for me this time? :-)
Let's just say my laptop is on quarantine this week.
I promise I'll do it next week then (and learn how to do it in the process).