etc/settings
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  ###