Re: [PATCH] bootstrap: add hooks for user-defined command-line options

[Jose E. Marchesi]

> Thanks, I installed that in your name.

Thank you.