On Tue, 15 Sep 2020, Guillem Jover wrote: [...] > From the error message printed, it looks like your temporary directory > is not big enough. If you set TMPDIR to something else it should work > I guess?
Argh! That's it. Sorry for missing it. The bug can be closed then. -- Francois Gouget <[email protected]>

