diff options
author | Adam Chlipala <adam@chlipala.net> | 2011-12-03 10:07:50 -0500 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2011-12-03 10:07:50 -0500 |
commit | f944c1f6dd0f0161b7e8aa5d6f8dbc721164d462 (patch) | |
tree | 7fe3656b0f0300748881c9f8c8e8f2d5ead67dae /lib/js | |
parent | 2286c970ce9d32a630e289df2685dbdff8e18217 (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.js | 17 |
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; |