> That’s good. If you had contributed before we might have had to get
you to assign copyright, but since it’s a small change we can let it
go. If you do decide to contribute again in the future you may have to
go through the process of assigning copyright.

Thank you for your pushing my change. I'll be careful.