On Tue Oct 11 13:56:49 2022 +0000, Mark Jansen wrote:
Ah, I completely missed that. Do you want me to amend this to the existing commit, or push a new commit? Should I rebase on the latest master when pushing?
Please amend the exisiting commit, rebase, and force push.