changeset 58781 | 0e41f26a0250 |
parent 58007 | 27778363775d |
child 58783 | ff534238d9b8 |
1.1 --- a/etc/settings Mon Jun 30 09:31:32 2014 +0200 1.2 +++ b/etc/settings Mon Jun 30 09:43:44 2014 +0200 1.3 @@ -26,9 +26,7 @@ 1.4 ### Interactive sessions (cf. isabelle tty) 1.5 ### 1.6 1.7 -ISABELLE_LINE_EDITOR="" 1.8 -[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)" 1.9 -[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)" 1.10 +ISABELLE_LINE_EDITOR="rlwrap" 1.11 1.12 1.13 ###