mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml
1.1 --- a/Admin/mira.py Wed Oct 10 22:53:48 2012 +0200
1.2 +++ b/Admin/mira.py Thu Oct 11 00:13:21 2012 +0200
1.3 @@ -119,11 +119,6 @@
1.4 # misc preparations
1.5 if 'lxbroy10' in misc.hostnames(): # special settings for lxbroy10
1.6 more_settings += '''
1.7 -ML_PLATFORM="x86_64-linux"
1.8 -ML_HOME="/home/polyml/polyml-5.4.1/x86_64-linux"
1.9 -ML_SYSTEM="polyml-5.4.1"
1.10 -ML_OPTIONS="-H 4000 --gcthreads 4"
1.11 -
1.12 ISABELLE_GHC="/usr/bin/ghc"
1.13 '''
1.14