# HG changeset patch
# User wenzelm
# Date 1393081883 -3600
# Node ID a99f9beba83ae1746a40d1fc7969c3545728e1ca
# Parent  cc350eb1087ec7bdfbb33b6d0053ed332053ab7c
tuned comment;

diff -r cc350eb1087e -r a99f9beba83a src/Tools/WWW_Find/etc/symbols
--- a/src/Tools/WWW_Find/etc/symbols	Sat Feb 22 15:07:33 2014 +0100
+++ b/src/Tools/WWW_Find/etc/symbols	Sat Feb 22 16:11:23 2014 +0100
@@ -1,4 +1,4 @@
-# Default interpretation of some Isabelle symbols
+# Default interpretation of some Isabelle symbols (outdated version for WWW_Find)
 
 \<zero>                 code: 0x01d7ec  group: digit
 \<one>                  code: 0x01d7ed  group: digit