Change client-side int parsing to match server-side, in ignoring initial zeroes

1 files changed, 17 insertions, 0 deletions

diff --git a/lib/js/urweb.js b/lib/js/urweb.js
index 015befa6..2dff3df6 100644
--- a/lib/js/urweb.js
+++ b/lib/js/urweb.js
@@ -944,7 +944,23 @@ function ssub(s, start, len) {
     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 pfl(s) {
 }
 
 function pio(s) {
+    s = trimZeroes(s);
     var r = parseInt(s);
     if (r.toString() == s)
         return r;