Re: [isabelle] ISABELLE_OUTPUT



Hi Lars,

Am 19.08.2014 um 16:09 schrieb Lars Hupel <hupel at in.tum.de>:

>  if [ -z "$ISABELLE_IDENTIFIER" ]; then
>    ISABELLE_HOME_USER="$USER_HOME/.isabelle"
>  else
>    ISABELLE_HOME_USER="$USER_HOME/.isabelle/$ISABELLE_IDENTIFIER"
>  fi
> 
> Is it actually possible to change this directory without touching
> 'etc/settings'?

Can't you just "$USER_HOME"? This is the usual trick, cf. the thread titled "Testboard problem" on "isabelle-dev" (4 to 7 July 2014).

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.