# HG changeset patch
# User wenzelm
# Date 1197663333 -3600
# Node ID 7726fbf5f81f7b11051ed920a6a107cacff32dd2
# Parent  3000965b1fdfea447b044460ddcab2ec7f6141d1
added ISABELLE_LINE_EDITOR;
tuned;

diff -r 3000965b1fdf -r 7726fbf5f81f etc/settings
--- a/etc/settings	Fri Dec 14 21:15:32 2007 +0100
+++ b/etc/settings	Fri Dec 14 21:15:33 2007 +0100
@@ -76,7 +76,16 @@
 
 
 ###
-### Compilation options (cf. isatool usedir)
+### Interactive sessions (cf. isatool tty)
+###
+
+ISABELLE_LINE_EDITOR=""
+[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p ledit)"
+[ -z "$ISABELLE_LINE_EDITOR" ] && ISABELLE_LINE_EDITOR="$(type -p rlwrap)"
+
+
+###
+### Batch sessions (cf. isatool usedir)
 ###
 
 ISABELLE_USEDIR_OPTIONS="-p 1 -v true -V outline=/proof,/ML"