equal
deleted
inserted
replaced
59 |
59 |
60 if [ -z "$INFILE" ]; then |
60 if [ -z "$INFILE" ]; then |
61 check_file "$ML_DBASE_PREFIX$ML_DBASE" |
61 check_file "$ML_DBASE_PREFIX$ML_DBASE" |
62 INFILE="$ML_DBASE" |
62 INFILE="$ML_DBASE" |
63 MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" |
63 MLTEXT="val use = PolyML.use; $EXIT $MLTEXT" |
64 case "$ML_SYSTEM" in |
64 DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max" |
65 polyml-4.1.[12]) |
|
66 DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S 180" |
|
67 ;; |
|
68 polyml-4.1.[34] | polyml-4.2.*) |
|
69 DISCGARB_OPTIONS="$DISCGARB_OPTIONS -S max" |
|
70 ;; |
|
71 esac |
|
72 else |
65 else |
73 COPYDB=true |
66 COPYDB=true |
74 fi |
67 fi |
75 |
68 |
76 if [ -z "$OUTFILE" ]; then |
69 if [ -z "$OUTFILE" ]; then |
91 fi |
84 fi |
92 |
85 |
93 |
86 |
94 ## run it! |
87 ## run it! |
95 |
88 |
96 case "$ML_SYSTEM" in |
|
97 polyml-4.1.[12]) |
|
98 ;; |
|
99 polyml-4.1.[34] | polyml-4.2.*) |
|
100 MLTEXT="PolyML.Compiler.printInAlphabeticalOrder := false; $MLTEXT" |
|
101 ;; |
|
102 esac |
|
103 |
|
104 if [ -z "$TERMINATE" ]; then |
89 if [ -z "$TERMINATE" ]; then |
105 FEEDER_OPTS="" |
90 FEEDER_OPTS="" |
106 else |
91 else |
107 FEEDER_OPTS="-q" |
92 FEEDER_OPTS="-q" |
108 fi |
93 fi |