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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
