changeset 26205 | 499f08293680 |
parent 25970 | 9053fd546501 |
child 26212 | 225b40bf36a7 |
1.1 --- a/etc/settings Wed Mar 05 21:48:15 2008 +0100 1.2 +++ b/etc/settings Wed Mar 05 22:48:50 2008 +0100 1.3 @@ -80,8 +80,8 @@ 1.4 ### 1.5 1.6 ISABELLE_LINE_EDITOR="" 1.7 +[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" 1.8 [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)" 1.9 -[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" 1.10 1.11 1.12 ###