# HG changeset patch
# User wenzelm
# Date 1207240956 -7200
# Node ID d65504ffb47dcddba7b382cc90dfef59400702fc
# Parent  188961eb1f082f6602ad51f91a7fc077c7ff7ab2
replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;

diff -r 188961eb1f08 -r d65504ffb47d src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Apr 03 18:42:34 2008 +0200
+++ b/src/Pure/General/symbol.ML	Thu Apr 03 18:42:36 2008 +0200
@@ -10,8 +10,8 @@
   type symbol
   val SOH: symbol
   val STX: symbol
-  val ETX: symbol
-  val EOT: symbol
+  val ENQ: symbol
+  val ACK: symbol
   val DEL: symbol
   val space: symbol
   val spaces: int -> string
@@ -87,8 +87,8 @@
 
 val SOH = chr 1;
 val STX = chr 2;
-val ETX = chr 3;
-val EOT = chr 4;
+val ENQ = chr 5;
+val ACK = chr 6;
 val DEL = chr 127;
 
 val space = chr 32;