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 |
--- a/etc/settings Wed Mar 05 21:48:15 2008 +0100 +++ b/etc/settings Wed Mar 05 22:48:50 2008 +0100 @@ -80,8 +80,8 @@ ### ISABELLE_LINE_EDITOR="" +[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" [ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)" -[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" ###