equal
deleted
inserted
replaced
17 } |
17 } |
18 |
18 |
19 |
19 |
20 ## prepare databases |
20 ## prepare databases |
21 |
21 |
22 EXIT="val exit = System.Unsafe.CInterface.exit;" |
22 if [ -z "$INFILE" ]; then |
|
23 INFILE="$ML_HOME/sml" |
|
24 EXIT="val exit = System.Unsafe.CInterface.exit;" |
|
25 else |
|
26 EXIT="" |
|
27 fi |
23 |
28 |
24 [ -z "$INFILE" ] && INFILE="$ML_HOME/sml" |
|
25 MOVE="" |
29 MOVE="" |
26 |
30 |
27 if [ -z "$OUTFILE" ]; then |
31 if [ -z "$OUTFILE" ]; then |
28 COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);' |
32 COMMIT='fun commit () = (output (std_err, "Error - Database is not opened for writing.\n"); false);' |
29 else |
33 else |