On 11/3/22 13:40, Karl Berry wrote:
Whatever happens, can one of you make the desired changes in gnulib?
Already done and installed, here: https://git.savannah.gnu.org/cgit/gnulib.git/commit/?id=ddfcbc95a6be3ddc588a93f21edb69cc7c214d9cAs part of that patch, I did the same sort of sync that you regularly do (and thanks for that).