lib/scripts/run-polyml
changeset 40544 34e56a6668ba
parent 40480 d695d258dfbc
child 41614 b7cd80330a16
     1.1 --- a/lib/scripts/run-polyml	Mon Nov 15 14:59:53 2010 +0100
     1.2 +++ b/lib/scripts/run-polyml	Mon Nov 15 15:41:58 2010 +0100
     1.3 @@ -9,24 +9,27 @@
     1.4  
     1.5  ## diagnostics
     1.6  
     1.7 +function fail()
     1.8 +{
     1.9 +  echo "$1" >&2
    1.10 +  exit 2
    1.11 +}
    1.12 +
    1.13  function fail_out()
    1.14  {
    1.15 -  echo "Unable to create output heap file: \"$OUTFILE\"" >&2
    1.16 -  exit 2
    1.17 +  fail "Unable to create output heap file: \"$OUTFILE\""
    1.18  }
    1.19  
    1.20  function check_file()
    1.21  {
    1.22 -  if [ ! -f "$1" ]; then
    1.23 -    echo "Unable to locate $1" >&2
    1.24 -    echo "Please check your ML system settings!" >&2
    1.25 -    exit 2
    1.26 -  fi
    1.27 +  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
    1.28  }
    1.29  
    1.30  
    1.31  ## compiler executables and libraries
    1.32  
    1.33 +[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
    1.34 +
    1.35  POLY="$ML_HOME/poly"
    1.36  check_file "$POLY"
    1.37