author | wenzelm |
Wed, 05 Mar 2008 22:48:50 +0100 | |
changeset 26205 | 499f08293680 |
parent 26204 | da9778392d8c |
child 26206 | 18194535f799 |
etc/settings | file | annotate | diff | comparison | revisions |
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 ###