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

2020-11-22 Thread Jose E. Marchesi
> Thanks, I installed that in your name. Thank you.

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

2020-11-22 Thread Paul Eggert
Thanks, I installed that in your name.

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

2020-11-22 Thread Bruno Haible
Can someone who actively uses 'bootstrap' please review this? Thanks. Jose E. Marchesi wrote in : > This patch adds a couple of hooks to the `bootstrap' script that > allows the users to handle their own command line options in

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

2020-11-18 Thread Jose E. Marchesi
This patch adds a couple of hooks to the `bootstrap' script that allows the users to handle their own command line options in their bootstrap.conf files. Usage example: bootstrap_option_hook () { case $1 in --jitter-srcdir) JITTER_SRCDIR=${$1#--jitter-srcdir=}; return 0;; esac return