[Dune] [Dune-Commit] dune-common r5537 - trunk/bin#

[Christian Engwer]

On Wed, Jun 10, 2009 at 01:12:38PM +0200, Sven Marnach wrote:
> Hi Christian,
> 
> christi at dune-project.org schrieb am Di, 09. Jun 2009, um 22:55:49 +0200:
> > save RESUME file in home directory
> 
> for me, this breaks things, because I have multiple DUNE trees
> (different versions) and they now all use the same resume file.  I
> often compile multiple trees in parallel and I would like to be able
> to resume either of them when things fail.
> 
> Before this patch, the resume feature worked fine.  What is the
> rationale for this patch?

An installed DUNE can't write to `basename $0`.

It was Martins proposal to have a resume feature and I told him that
it will be a lot of work implement it properly. I don't think we will
support your use pattern. You can still resume it, it is just that you
should not run an other one in between. But anyway the old version did
was not fool-proof, because it would still (and does still) allow you
to resume an old run with a different command. The proper way would be
to add stamp files for the different commands in the different
source/build directories.

Christian