#958 do not write random files to the user's home directory
Metadata
| Property | Value |
|---|---|
| Reported by | Andreas Lauser (andreas.lauser@iws.uni-stuttgart.de) |
| Reported at | Oct 4, 2011 15:54 |
| Type | Bug Report |
| Version | 2.1 |
| Operating System | Unspecified / All |
| Last edited by | Martin Nolte (nolte@mathematik.uni-freiburg.de) |
| Last edited at | Nov 11, 2011 10:33 |
| Closed by | Martin Nolte (nolte@mathematik.uni-freiburg.de) |
| Closed at | Nov 11, 2011 10:33 |
| Closed in version | Unknown |
| Resolution | Implemented |
| Comment |
Description
currently (which is dune 2.1 in my case) dunecontrol writes the file dune.resume to the user's home directory on every run and there is no way to stop it doing that. Beside the fact that this is very bad style, it breaks the build for cases where $HOME is not writable (e.g. running it under a Jenkins instance'). in the attachment you find a fix for this issue, which boils down to having to explicitly specify the RESUME_FILE if the --resume option ought to be used. let me know if you have any objections.