equal
deleted
inserted
replaced
210 |
210 |
211 ## run it! |
211 ## run it! |
212 |
212 |
213 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
213 ML_SYSTEM_BASE=$(echo "$ML_SYSTEM" | cut -f1 -d-) |
214 |
214 |
215 [ -n "$MODES" ] && MLTEXT="print_mode := [$MODES]; $MLTEXT" |
215 [ -n "$MODES" ] && MLTEXT="Unsynchronized.change print_mode (append [$MODES]); $MLTEXT" |
216 |
216 |
217 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();" |
217 [ -n "$SECURE" ] && MLTEXT="$MLTEXT Secure.set_secure ();" |
218 |
218 |
219 NICE="nice" |
219 NICE="nice" |
220 |
220 |