On Tue, Mar 31, 2020 at 5:14 PM Juan José García-Ripoll <
address@hidden> wrote:
> On a different email I was instructed to add this as a compile time
> option, which is what my patch does. Sorry if I did not follow all
> threads properly.
My quote is from this very thread. But of course it is easy to accidentally
skip things when threads get too long or some issue is simultaneously
discussed in several places at once.