Re: gendocs.sh in gnulib?

[Karl Berry]

    Is it OK to change the license to "GPLed build tool"?  

Sounds good to me.

    The output from the script isn't restricted, right?

Nah.  It's totally trivial.

Thanks,
k