Ian Jackson <ijackson@chiark.greenend.org.uk> writes: > I don't see it. Perhaps you failed to push. I have transposed it > into git myself and pushed. Indeed, I forgot to push. I'm sorry about that. :/ I'm clearly not at my best at the moment. I can confirm that Git found your change to be identical to mine, so everything should be good. -- Russ Allbery (rra@debian.org) <http://www.eyrie.org/~eagle/>