Am 14.09.2018 um 09:24 schrieb Sven Schreiber:
(And BTW, all this was with a compiled-from-git version from last
month. Perhaps eventually we should check whether the standard version
shipped with Ubuntu has the same problems.)
I tested this on a virtual machine running 18.04 and installing the
standard gretl package (based on 2017d), and in a quick test I didn't
see any problems. So fortunately the problem is less severe than I
thought at first.