equal
deleted
inserted
replaced
29 |
29 |
30 ## process command line |
30 ## process command line |
31 |
31 |
32 # options |
32 # options |
33 |
33 |
34 declare -a SERVER_OPTS=() |
34 declare -a SERVER_OPTS=(-s -c) |
35 |
35 |
36 while getopts "n:p:" OPT |
36 while getopts "n:p:" OPT |
37 do |
37 do |
38 case "$OPT" in |
38 case "$OPT" in |
39 n) |
39 n) |
60 |
60 |
61 # main |
61 # main |
62 |
62 |
63 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null |
63 if type -p "$ISABELLE_LINE_EDITOR" > /dev/null |
64 then |
64 then |
65 exec "$ISABELLE_LINE_EDITOR" isabelle server -s -C "${SERVER_OPTS[@]}" |
65 exec "$ISABELLE_LINE_EDITOR" isabelle server "${SERVER_OPTS[@]}" |
66 else |
66 else |
67 echo "### No line editor: \"$ISABELLE_LINE_EDITOR\"" |
67 echo "### No line editor: \"$ISABELLE_LINE_EDITOR\"" |
68 exec isabelle server -s -C "${SERVER_OPTS[@]}" |
68 exec isabelle server "${SERVER_OPTS[@]}" |
69 fi |
69 fi |