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