On Thu, Dec 20, 2018 at 05:23:59PM +0100, Jürgen Spitzmüller wrote: > Am Donnerstag, den 20.12.2018, 17:19 +0100 schrieb Enrico Forestieri: > > This is not what the reporter of #11415 meant. > > ... in your reading.
Maybe. However, I wonder how many read it (want it) in the same way. -- Enrico