A suitably kludgy fix for this issue has now been committed to HEAD.
This archive was generated by hypermail 2.4.0 : Wed May 19 2021 - 11:39:44 UTC