parse_attrib: proper index of name end!
authorwenzelm
Thu, 21 Aug 2008 22:06:17 +0200
changeset 27946 ec706ad37564
parent 27945 d2dc5a1903e8
child 27947 b6dc0a396857
parse_attrib: proper index of name end!
src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Thu Aug 21 21:42:16 2008 +0200
+++ b/src/Pure/General/yxml.scala	Thu Aug 21 22:06:17 2008 +0200
@@ -61,7 +61,7 @@
     val s = source.toString
     val i = s.indexOf('=')
     if (i <= 0) err_attribute()
-    (s.substring(0, i - 1), s.substring(i + 1))
+    (s.substring(0, i), s.substring(i + 1))
   }