On Wed, Dec 7, 2022 at 7:17 PM Eli Zaretskii <eliz@gnu.org> wrote:

> If that require is not needed,

It isn't. It was just added to help fix a problem that wasn't fixed.

> there should be no problem removing it.

Release branch, or master?