diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2009-05-26 12:25:06 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2009-05-26 12:25:06 -0400 |
| commit | d4748e41f7fc4865db89ebac0c7f646dca82f89a (patch) | |
| tree | 53e0b285bbcb0e28d3cbbd507da21fcc41d8995e /lib/js | |
| parent | 19e4ef1a48aafbb7035af03324b9ff07b3474230 (diff) | |
Chars and more string operations
Diffstat (limited to 'lib/js')
| -rw-r--r-- | lib/js/urweb.js | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/lib/js/urweb.js b/lib/js/urweb.js index c031678a..2b4d2643 100644 --- a/lib/js/urweb.js +++ b/lib/js/urweb.js @@ -351,6 +351,9 @@ function eh(x) { function ts(x) { return x.toString() } function bs(b) { return (b ? "True" : "False") } +function sub(x, i) { return x[i]; } +function suf(x, i) { return x.substring(i); } + function pi(s) { var r = parseInt(s); if (r.toString() == s) |