lib/scripts/run-poplogml
changeset 17820 9822a7755ad4
parent 17807 cc5dbc24e561
equal deleted inserted replaced
17819:1241e5d31d5b 17820:9822a7755ad4
    65 procedure(str) with_props use_string;
    65 procedure(str) with_props use_string;
    66         lvars str;
    66         lvars str;
    67         lconstant UseExn = exception("Use");
    67         lconstant UseExn = exception("Use");
    68 
    68 
    69         define dlocal pop_exception_handler(n, msg, idstring, severity);
    69         define dlocal pop_exception_handler(n, msg, idstring, severity);
       
    70                 [n ^n msg ^msg  idstring ^idstring severity ^severity] ==>
    70                 returnunless(severity == `E` or severity == `R`)(false);
    71                 returnunless(severity == `E` or severity == `R`)(false);
    71                 erasenum(n);
    72                 erasenum(n);
    72                 raise(UseExn(str));
    73                 raise(UseExn(str));
    73         enddefine;
    74         enddefine;
    74 
    75 
   120 "$POPLOG" pml "$DB" $ML_OPTIONS -load "$INIT" 2>&1
   121 "$POPLOG" pml "$DB" $ML_OPTIONS -load "$INIT" 2>&1
   121 RC="$?"
   122 RC="$?"
   122 
   123 
   123 rm -f "$INIT"
   124 rm -f "$INIT"
   124 
   125 
   125 [ -n "$OUTFILE" ] && check_heap_file "$OUTFILE" && \
   126 if [ -n "$OUTFILE" ] && check_heap_file "$OUTFILE"; then
   126   [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
   127   [ -n "$NOWRITE" ] && chmod -w "$OUTFILE"
       
   128   rm -f "$OUTFILE-"
       
   129 fi
   127 
   130 
   128 exit "$RC"
   131 exit "$RC"