changeset 49814 | 0aaed83532e1 |
parent 49813 | fe9eb2b5c1ec |
child 50593 | 8372c8b59cea |
--- a/Admin/mira.py Wed Oct 10 22:53:48 2012 +0200 +++ b/Admin/mira.py Thu Oct 11 00:13:21 2012 +0200 @@ -119,11 +119,6 @@ # misc preparations if 'lxbroy10' in misc.hostnames(): # special settings for lxbroy10 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 4000 --gcthreads 4" - ISABELLE_GHC="/usr/bin/ghc" '''