[isabelle-dev] Testboard problem
Makarius
makarius at sketis.net
Mon Jul 7 12:23:30 CEST 2014
On Mon, 7 Jul 2014, Lars Noschinski wrote:
>>> @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.
> I have implemented this approach (i.e., Mira sets $USER_HOME to some
> arbitrary place before starting Isabelle) and this seems to work. The
> only open question is whether you see any problems in $HOME /= $USER_HOME.
It should work. The whole point of USER_HOME is to allow this to be
different from HOME, which has slightly different meaning on Windows +
Cygwin.
Makarius
More information about the isabelle-dev
mailing list