etc/settings
changeset 15865 222092a48131
parent 15846 6f24b0c36dbd
child 15880 d6aa6c707acf
equal deleted inserted replaced
15864:cc1b4a289321 15865:222092a48131
    32   # maybe a shrink-wrapped polyml on x86-linux ...
    32   # maybe a shrink-wrapped polyml on x86-linux ...
    33 
    33 
    34   # Poly/ML 4.0, 4.1, 4.1.x
    34   # Poly/ML 4.0, 4.1, 4.1.x
    35   # include version number, needed for choosing right options
    35   # include version number, needed for choosing right options
    36   # If automatic setting doesn't work, use e.g. ML_VERSION=4.1.3
    36   # If automatic setting doesn't work, use e.g. ML_VERSION=4.1.3
    37   ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly --version  | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p')
    37   ML_VERSION=$(echo "OS.Process.exit OS.Process.success;" | /usr/bin/poly | sed -n 's,.*Poly/ML[ ]*\([^ ]*\)[ ]*Release,\1,p')
    38   ML_SYSTEM=polyml-${ML_VERSION}
    38   ML_SYSTEM=polyml-${ML_VERSION}
    39   # processor/OS type
    39   # processor/OS type
    40   ML_PLATFORM=x86-linux
    40   ML_PLATFORM=x86-linux
    41   # where to find binaries
    41   # where to find binaries
    42   ML_HOME=/usr/bin
    42   ML_HOME=/usr/bin