# HG changeset patch # User wenzelm # Date 1326407343 -3600 # Node ID 4a892432e8f16b1957ef2b89379868e7750d63c4 # Parent 9d2273d50f4fe92c2555552e2c1acae3d012f876 more modest settings for lxbroy10 -- might actually perform better; diff -r 9d2273d50f4f -r 4a892432e8f1 Admin/mira.py --- a/Admin/mira.py Thu Jan 12 22:05:54 2012 +0100 +++ b/Admin/mira.py Thu Jan 12 23:29:03 2012 +0100 @@ -201,15 +201,14 @@ def isabelle_makeall(env, case, paths, dep_paths, playground, usedir_options=default_usedir_options, more_settings='', target='all', make_options=()): - # FIXME!? if 'lxbroy10' in misc.hostnames(): make_options += ('-j', '8') - usedir_options += " -M 6 -q 2 -i false -d false" + usedir_options += " -M 4 -q 2 -i false -d false" more_settings += ''' ML_PLATFORM="x86_64-linux" ML_HOME="/home/polyml/polyml-5.4.1/x86_64-linux" ML_SYSTEM="polyml-5.4.1" -ML_OPTIONS="-H 8000 --gcthreads 6" +ML_OPTIONS="-H 4000 --gcthreads 4" ISABELLE_GHC="/usr/bin/ghc" '''