Commit dc08febea1fc0a8c902dfa89d0abc2952873529b

Bruno Haible 2021-12-13T03:03:13

gnulib-tool: Fix mistake in last commit.