[Termtools] use $TMPDIR, not /tmp - Re: possible problems (permission denied)

[Johannes Waldmann]

Regarding the problem mentioned here:
http://lists.lri.fr/pipermail/termtools/2015-August/001082.html
Aaron tells me:

> The permission denied message is for accessing
> a file in /tmp/.  Now, we are setting the TMPDIR
> environment variable to a suitable temporary directory,
> with plenty of space.  So tools that follow the linux
> convention of creating temporary files in the directory
> specified by TMPDIR should not have a problem.
> I cannot be sure, but one thing that would explain
> the error is if the user's solver were trying to write
> a large file to /tmp.  It only has 2GB in that file system.
> That is why we are specifying TMPDIR.

- J.