[Termtools] starexec introduces noise, results in ERROR

[Johannes Waldmann]

> In case the 'rm' instructions are part of muTerm's start script, 

They are not?

https://www.starexec.org/starexec/secure/details/configuration.jsp?id=326595

There is one "rm" but it's in the end,
and for a different file, and for just one.


The "job log" has the following. The offending messages are visible.
I think that would not happen if it'd be stdout/err
produced by the tool.


06/23/20 02:54:34 AM CDT: Running runsolver.
...
06/23/20 02:56:56 AM CDT: Runsolver finished.
...
06/23/20 02:56:56 AM CDT: recording header of job pair output
rm: cannot remove ‘/tmp/muTerm5117023052084420925.in.dec’: No such file
or directory
rm: cannot remove ‘/tmp/muTerm5117023052084420925.in.form’: No such file
or directory


- J