summaryrefslogtreecommitdiff
path: root/lib/js
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-12-03 10:07:50 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2011-12-03 10:07:50 -0500
commitf944c1f6dd0f0161b7e8aa5d6f8dbc721164d462 (patch)
tree7fe3656b0f0300748881c9f8c8e8f2d5ead67dae /lib/js
parent2286c970ce9d32a630e289df2685dbdff8e18217 (diff)
Change client-side int parsing to match server-side, in ignoring initial zeroes
Diffstat (limited to 'lib/js')
-rw-r--r--lib/js/urweb.js17
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;