[isabelle-dev] Testboard problem

[Makarius]

On Wed, 4 Jun 2014, Lars Noschinski wrote:

> On 04.06.2014 13:37, Johannes Hölzl wrote:
>> We remove ~isatest/.isabelle/heaps/.../HOL-Proofs on lxbroy10 and now it
>> works...
>>
>> I don't know why mira is accessing this file, it actually sets up the
>> settings file to _not_ look into the users heaps-directory. But it looks
>> like there is a problem with this setup.
> After looking a bit closer: Mira changes ISABELLE_HOME_USER (by
> appending it to $ISABELLE_HOME/etc/settings). Of course, this is too
> late to affect ISABELLE_PATH, which still refers to
> $USER_HOME/.isabelle/heaps.
>
> So, we set $USER_HOME instead before starting Isabelle (see
> bcc6dc6c1d1c8a6).
>
> @Makarius: Does this use fit the intention of USER_HOME?

Is this question still open?  I have lost track of the various Mira
configuration problems.


 	Makarius