On 05.04.2023 18:39, Julien Grall wrote: > To reduce the amount of patch to resend, I was actually thinking to > merge patch #1-3 and #5 (so leave this patch alone) and modify the > default in a follow-up. Any thoughts?
Well, yes, that's what I did a couple of days ago already. Jan