On Sunday, June 26, 2022, Paul Smith <psm...@gnu.org> wrote > > > I would prefer to have that fixed in gnulib, than continue to maintain > a local copy just to avoid this issue.
Then there is no choice to drop gnulib and build.sh should go. Since you asked for opinions, my opinion is that maintaining a mini make along with the real make can complicate the release procedure. It is not clear that anybody would benefit from a mini make. What was the original driving force to introduce build.sh? > Seems like it's not so much that the patch was rejected; indeed they > seem to agree there's a bug. But they wanted more work on it and it > sort of fell apart. I have no idea how much effort it would be to push > hard enough to get a change merged. > > > > >
