Re: "make dist" fails

[Bruno Haible via Bug reports for the GNU Texinfo documentation system]

Patrice Dumas wrote:
> Something like that is done in:
> https://cgit.git.savannah.gnu.org/cgit/texinfo.git/commit/?id=5f71ebf52737eef14fc1c7ad02390a38a3bbeb92

Thanks. The "make dist" step in the CI is now succeeding again, and the CI
run is progressing.

Bruno