sS js_setDivContents(S divID, S contents) {
  ret replaceDollarVars_js([[
    {
      var div = document.getElementById($divID);
      if (div)
        div.innerHTML = $contents;
    }
  ]], +divID, +contents);
}