# HG changeset patch
# User wenzelm
# Date 1478767395 -3600
# Node ID 8be21ca788ca9d46bd159e02fdf9f9ffd759c58f
# Parent  62c807eb009f41a46b5156bebab05e9a4e25ab70
tuned comment;

diff -r 62c807eb009f -r 8be21ca788ca src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Wed Nov 09 22:23:36 2016 +0100
+++ b/src/Pure/General/symbol.scala	Thu Nov 10 09:43:15 2016 +0100
@@ -197,7 +197,7 @@
   }
 
 
-  /* text chunks */
+  /* symbolic text chunks -- without actual text */
 
   object Text_Chunk
   {