This is of interest to us: https://github.com/micropython/micropython/pull/13219, merged instead of https://github.com/micropython/micropython/pull/13035.