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=ddfcbc95a6be3ddc588a93f21edb69cc7c214d9c

As part of that patch, I did the same sort of sync that you regularly do (and thanks for that).

Reply via email to