Re: [PATCH] gnulib-tool.py: Comment out undefined variable.

[Bruno Haible]

Collin Funk wrote:
> It seems that your commit 01cd78f9d682ff75cc5ab1c2d21b911bdd9215b8
> accidentally caused this. While cleaning up the handling of paths, I
> think you accidentally removed this variable.

Yep. Thanks for the fix! Applied.

Bruno