sS js_replaceHTML(S html) {
  ret replaceDollarVars_js([[
    (function() {
      var target = document.querySelector("html");
      target.innerHTML = $html;
      nodeScriptReplace(target);
    })(); ]], html := unnull(html));
}