On 8/1/2018 10:06 PM, Johannes Pfau wrote: > I guess that would be acceptable if there is a real benefit, but I have > not seen a single argument for the current behavior in this thread. Please read my postings in this thread, then.