# HG changeset patch
# User krauss
# Date 1349907201 -7200
# Node ID 0aaed83532e1f4e52ee6967a9990ec7c23c290ad
# Parent  fe9eb2b5c1ec6bea5d49aa111d34d1794758e3e2
mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml

diff -r fe9eb2b5c1ec -r 0aaed83532e1 Admin/mira.py
--- 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"
 '''