# HG changeset patch
# User wenzelm
# Date 1204753730 -3600
# Node ID 499f08293680bb2132c834c8b8cf589d03d7b4cc
# Parent  da9778392d8c2f995f4b3544cd30068a3d8d9add
ISABELLE_LINE_EDITOR: prefer rlwrap, which passes interrupts properly;

diff -r da9778392d8c -r 499f08293680 etc/settings
--- 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)"
 
 
 ###