Re: Problem with tmpdir usage

[Nelson A. de Oliveira]

On Tue, Jul 29, 2014 at 4:19 PM, Ole Tange <o...@tange.dk> wrote:
> Yep. It seems you have found a bug.

Do you need it reported somewhere else or can I consider it done? :-)