equal
deleted
inserted
replaced
1 #!/bin/bash |
1 #!/bin/bash |
|
2 # |
|
3 # $Id$ |
2 # |
4 # |
3 # Poly/ML startup script. |
5 # Poly/ML startup script. |
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 22-Nov-1996, MMW 25-Nov-1996 |
|
11 |
9 |
12 |
10 |
13 ## diagnostics |
11 ## diagnostics |
14 |
12 |
15 function fail() |
13 function fail() |
26 ML_DBASE=$ML_HOME/ML_dbase |
24 ML_DBASE=$ML_HOME/ML_dbase |
27 POLY=$ML_HOME/poly |
25 POLY=$ML_HOME/poly |
28 DISCGARB=$ML_HOME/discgarb |
26 DISCGARB=$ML_HOME/discgarb |
29 |
27 |
30 case "$ML_SYSTEM" in |
28 case "$ML_SYSTEM" in |
31 polyml-2.07) |
|
32 ;; |
|
33 polyml-3.1) |
29 polyml-3.1) |
34 DISCGARB="$ML_HOME/discgarb -c" |
30 DISCGARB="$DISCGARB -c" |
35 export LM_LICENSE_FILE=$ML_HOME/license.dat |
31 export LM_LICENSE_FILE=$ML_HOME/license.dat |
36 ;; |
|
37 *) |
|
38 fail "Unknown ML system: \"$ML_SYSTEM\"" |
|
39 ;; |
32 ;; |
40 esac |
33 esac |
41 |
34 |
42 |
35 |
43 |
36 |
85 $START_POLY |
78 $START_POLY |
86 RC=$? |
79 RC=$? |
87 else |
80 else |
88 TMP_FILE=/tmp/mltext-$$ |
81 TMP_FILE=/tmp/mltext-$$ |
89 echo "$MLTEXT" >$TMP_FILE |
82 echo "$MLTEXT" >$TMP_FILE |
90 cat $TMP_FILE - | $START_POLY |
83 $ISABELLE_HOME/lib/scripts/ucat $TMP_FILE - | $START_POLY |
91 RC=$? |
84 RC=$? |
92 rm $TMP_FILE |
85 rm $TMP_FILE |
93 fi |
86 fi |
94 |
87 |
95 [ $RC -a -n "$OUTFILE" ] && $DISCGARB "$OUTFILE" |
88 [ $RC -eq 0 -a -n "$OUTFILE" ] && $DISCGARB "$OUTFILE" |
96 |
89 |
97 exit $RC |
90 exit $RC |