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