# HG changeset patch
# User wenzelm
# Date 1219349177 -7200
# Node ID ec706ad3756487c6b6b003dda2b5b66b1319d97a
# Parent  d2dc5a1903e89de2009ab7fd59e69c5950a08b4e
parse_attrib: proper index of name end!

diff -r d2dc5a1903e8 -r ec706ad37564 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))
   }