> In general you have to remember when adding a new option and/or > documentation for a new option to run make regenerate-opt-urls. But if > you forget and push the change without the opt.urls change a friendly > bot should remind you and even produce a diff that you can use to fix > things up.
Indeed, I did not notice that the bot's outcome was "failed", thanks. -- Eric Botcazou
