| changeset 6285 | 112a15c311f0 |
| parent 5965 | f91212fd2c7c |
| child 7459 | 173efad74891 |
| 6284:147db42c1009 | 6285:112a15c311f0 |
|---|---|
86 do |
86 do |
87 [ -f "$FILE" ] && ARGS="$ARGS -l $FILE" |
87 [ -f "$FILE" ] && ARGS="$ARGS -l $FILE" |
88 done |
88 done |
89 |
89 |
90 ARGS="$ARGS -f isabelle" |
90 ARGS="$ARGS -f isabelle" |
91 |
91 exec $PROGNAME -T "Isabelle" $ARGS |
92 |
|
93 exec $PROGNAME -T "Isabelle" -geometry $MAINGEOM $ARGS |