[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