Am 02.07.2021 um 02:39 schrieb Ton:
> Hallo Christoph, just created two pull requests. I hope everything on my side
> was done OK, first time I've done this.
No formal complaints from my side - again, thanks!
There's one remaining issue that needs to be ironed out, and I've got a
few suggestions for additional changes that you could also throw in
along the way. See my comments to the v3.7 pull request (most also apply
As for the "git-technical" side, this should be fairly straightforward:
All you'll have to do is push additional commits to the corresponding
branches of your repo copy, and the pull requests should automatically
pick those up and update themselves accordingly.
Post a reply to this message