changeset 3637 | 02ba2acc69c3 |
parent 3596 | c44c83006891 |
child 3689 | 73378599a65b |
--- a/etc/settings Thu Aug 07 23:35:32 1997 +0200 +++ b/etc/settings Thu Aug 07 23:37:53 1997 +0200 @@ -58,8 +58,10 @@ #A hack! 'build' tells us store heaps within the distribution. if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then ISABELLE_OUTPUT=$ISABELLE_HOME/heaps + ISABELLE_BROWSER_INFO=$ISABELLE_HOME/browser_info else ISABELLE_OUTPUT=$ISABELLE_HOME_USER/heaps + ISABELLE_BROWSER_INFO=$ISABELLE_HOME_USER/browser_info fi #Users may want to change this.