# HG changeset patch
# User wenzelm
# Date 1197045606 -3600
# Node ID ee11881606b7d338710efa0ffa06f5c12581d702
# Parent  fee953b4501554b31557c9a6348b92b02c0f7ff0
special_end: replaced Z by dot;

diff -r fee953b45015 -r ee11881606b7 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Fri Dec 07 17:40:05 2007 +0100
+++ b/src/Pure/Tools/isabelle_process.ML	Fri Dec 07 17:40:06 2007 +0100
@@ -31,7 +31,7 @@
 local
 
 fun special c = chr 2 ^ c;
-val special_end = special "Z";
+val special_end = special ".";
 
 fun output c m s =
   Output.writeln_default (special c ^ Markup.enclose m s ^ special_end);