On 2020-08-14 11:33 a.m., Tom Tromey wrote: > Simon> All right, here's the same patch with a commit log and ChangeLog > Simon> entry. > > Looks good, thank you. > > Tom > Thanks, I pushed it. Simon