etc/settings
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.