Sorry, I never tested whether the setting actually persists; I just hoped that it would. But indeed it is not; I had to manually intervene once again.
Jordi's analysis and patch look plausible to me. It might be slightly
better to compare "${GRUB_DISABLE_OS_PROBER}" to "true" instead of
"false" (swapping the branches of the conditional), since that's what
/etc/grub.d/30_os-prober does.
Thanks,
Bertram
