mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml
authorkrauss
Thu, 11 Oct 2012 00:13:21 +0200
changeset 508290aaed83532e1
parent 50828 fe9eb2b5c1ec
child 50830 e4f87bd5f223
child 50837 0cfc1651be25
mira: discontinued special settings for lxbroy10, which are probably made obsolete by newer polyml
Admin/mira.py
     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