[Dune] [#958] do not write random files to the user's home directory

[Dune]

THIS IS AN AUTOMATED MESSAGE, DO NOT REPLY.

The following task has a new comment added:

FS#958 - do not write random files to the user's home directory
User who did this - Jö Fahlke (joe)

----------
@Elias: Yes, you will get a problem when you run instances of dunecontrol
concurrently for different build trees, and then try to resume from the
resulting .dune.resume.  I never claimed otherwise.

My point was that there is no straightforward way for dunecontrol to have
different default .dune.resume files for different build trees, since there is
no way to automatically identify what a build tree actually is.  Therefore the
only reasonable options are

 a) have one default .dune.resume in a fixed location,

 b) have a .dune.resume in the current directory by default,

 c) have no .dune.resume by default.

If you chose a) you have the problem of concurrent build, no matter where
exactly you put that file (this was what I meant that the question of the
location and the problem of concurrency are orthogonal).  Choosing b) may be a
bit better but it gives you no guarantee the concurrency problem is avoided.
The location of the modules can be given via the opts-file or the environment,
so you can run dunecontrol two times for different build trees from the same
directory.

----------

More information can be found at the following URL:
http://www.dune-project.org/flyspray/index.php?do=details&task_id=958#comment2765

You are receiving this message because you have requested it from the Flyspray bugtracking system.  If you did not expect this message or don't want to receive mails in future, you can change your notification settings at the URL shown above.