etc/settings
changeset 15734 56a807868e23
parent 15717 541e50adfc73
child 15779 aed221aff642
equal deleted inserted replaced
15733:75b9219980d3 15734:56a807868e23
    31 elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
    31 elif [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
    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   ML_SYSTEM=polyml-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')
       
    38   ML_SYSTEM=polyml-${ML_VERSION}
    37   # processor/OS type
    39   # processor/OS type
    38   ML_PLATFORM=x86-linux
    40   ML_PLATFORM=x86-linux
    39   # where to find binaries
    41   # where to find binaries
    40   ML_HOME=/usr/bin
    42   ML_HOME=/usr/bin
    41   # where to find the standard database
    43   # where to find the standard database