manifestXmlJsonml doesn't work with numerical attributes

[fugu13]

With the example from the standard library docs (reproduced below), manifestXmlJsonml fails with Cannot call manifestXmlJsonml on class ujson.Num.

The example:

std.manifestXmlJsonml([
  'svg', { height: 100, width: 100 },
  [
    'circle', {
      cx: 50, cy: 50, r: 40,
       stroke: 'black', 'stroke-width': 3,
       fill: 'red',
    }
  ],
])

Per the docs, the expected value is XML equivalent to:

<svg height="100" width="100">
  <circle cx="50" cy="50" fill="red" r="40"
  stroke="black" stroke-width="3"></circle>
</svg>

I've verified that's the return value in the jsonnet.org editable text areas.