Hi,

Maybe this problem never triggers.  It is a « better be safe » kind of
patch.