# HG changeset patch
# User wenzelm
# Date 1238494037 -7200
# Node ID a0863fcd9bbfe50f30ab9466e7875635df007028
# Parent  7d02340f095d27d2acdca51b1f33ebfa26e1a70c
suggest HOL_USEDIR_OPTIONS="-p 2 -Q false", which is more likely to work within the limits of 32 bit address space;

diff -r 7d02340f095d -r a0863fcd9bbf etc/settings
--- a/etc/settings	Tue Mar 31 11:11:36 2009 +0200
+++ b/etc/settings	Tue Mar 31 12:07:17 2009 +0200
@@ -94,7 +94,7 @@
 
 # Specifically for the HOL image
 HOL_USEDIR_OPTIONS=""
-#HOL_USEDIR_OPTIONS="-p 2"
+#HOL_USEDIR_OPTIONS="-p 2 -Q false"
 
 #Source file identification (default: full name + date stamp)
 ISABELLE_FILE_IDENT=""