equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
|
2 # |
|
3 # $Id$ |
2 # |
4 # |
3 # SML/NJ startup script (for 1.06 or later). |
5 # SML/NJ startup script (for 1.06 or later). |
4 # |
6 # |
5 # $Id$ |
|
6 # |
|
7 # Global vars: INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE, |
7 # Global vars: INFILE OUTFILE COPYDB MLTEXT OPTIONS TERMINATE, |
8 # and from settings |
8 # and from settings |
9 # |
|
10 # MMW 30-Nov-1996 |
|
11 |
9 |
12 |
10 |
13 ## diagnostics |
11 ## diagnostics |
14 |
12 |
15 function fail() |
13 function fail() |
60 $START_SML |
58 $START_SML |
61 RC=$? |
59 RC=$? |
62 else |
60 else |
63 TMP_FILE=/tmp/mltext-$$ |
61 TMP_FILE=/tmp/mltext-$$ |
64 echo "$MLTEXT" >$TMP_FILE |
62 echo "$MLTEXT" >$TMP_FILE |
65 cat $TMP_FILE - | $START_SML |
63 $ISABELLE_HOME/lib/scripts/ucat $TMP_FILE - | $START_SML |
66 RC=$? |
64 RC=$? |
67 rm $TMP_FILE |
65 rm $TMP_FILE |
68 fi |
66 fi |
69 |
67 |
70 exit $RC |
68 exit $RC |