equal
deleted
inserted
replaced
17 # ISABELLECOMP: the ML compiler |
17 # ISABELLECOMP: the ML compiler |
18 |
18 |
19 # A typical shell script for /bin/sh is... |
19 # A typical shell script for /bin/sh is... |
20 # ML_DBASE=/usr/groups/theory/poly2.04/`arch`/ML_dbase |
20 # ML_DBASE=/usr/groups/theory/poly2.04/`arch`/ML_dbase |
21 # ISABELLEBIN=/homes/`whoami`/bin |
21 # ISABELLEBIN=/homes/`whoami`/bin |
22 # ISABELLECOMP="poly -noDisplay" |
22 # ISABELLECOMP="/usr/bin/poly -noDisplay" |
23 # export ML_DBASE ISABELLEBIN ISABELLECOMP |
23 # export ML_DBASE ISABELLEBIN ISABELLECOMP |
24 # nohup make-all $* |
24 # nohup make-all $* |
25 |
25 |
26 set -e #fail immediately upon errors |
26 set -e #fail immediately upon errors |
27 |
27 |