# HG changeset patch
# User wenzelm
# Date 1404115832 -7200
# Node ID ff534238d9b89f10867853dd9cd5de32fb2de04f
# Parent  802d33c46459437f481ca5260212178cbed7be1e
tuned comments;

diff -r 802d33c46459 -r ff534238d9b8 etc/settings
--- a/etc/settings	Mon Jun 30 10:00:16 2014 +0200
+++ b/etc/settings	Mon Jun 30 10:10:32 2014 +0200
@@ -23,7 +23,7 @@
 
 
 ###
-### Interactive sessions (cf. isabelle tty)
+### Interactive sessions (cf. isabelle console)
 ###
 
 ISABELLE_LINE_EDITOR="rlwrap"