Date: Mon, 4 Sep 2023 21:43:25 -0700
Cc: "Trent W. Buck" <trentbuck@gmail.com>,
Philip Kaludercic <philipk@posteo.net>, Eli Zaretskii <eliz@gnu.org>,
gregory@heytings.org, 62370-done@debbugs.gnu.org
From: Jim Porter <jporterbugs@gmail.com>
As such, I've pushed this to the master branch as f08684ab39d. Closing
this now. (Of course, if this *does* cause some problems, we can revisit
this.)
Please in the future allow more time for the "interested parties" to
respond (and maybe even ask them directly). At the beginning of this
discussion I asked to hear more opinions, after expressing my own
hesitation, so it would be prudent to let me chime in and say whether
I'm okay with the change before installing the changes right after
Stefan said he agreed with you...