# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1322924870 18000
# Node ID 62d6d452c2b82a49bda47ed9a3eeb12901c6033f
# Parent  43f22a8f76cc939430736da56b59a63a8eddeed2
Change client-side int parsing to match server-side, in ignoring initial zeroes

diff -r 43f22a8f76cc -r 62d6d452c2b8 lib/js/urweb.js
--- a/lib/js/urweb.js	Sat Dec 03 10:00:10 2011 -0500
+++ b/lib/js/urweb.js	Sat Dec 03 10:07:50 2011 -0500
@@ -944,7 +944,23 @@
     return s.substring(start, start+len);
 }
 
+function trimZeroes(s) {
+    for (var i = 0; i < s.length; ++i)
+        if (s[i] != '0') {
+            if (i > 0)
+                return s.substring(i);
+            else
+                return s;
+        }
+
+    if (s == "0")
+        return s;
+    else
+        er("Can't parse int: " + s);
+}
+
 function pi(s) {
+    s = trimZeroes(s);
     var r = parseInt(s);
     if (r.toString() == s)
         return r;
@@ -961,6 +977,7 @@
 }
 
 function pio(s) {
+    s = trimZeroes(s);
     var r = parseInt(s);
     if (r.toString() == s)
         return r;