sS jsReplaceTitle(S title) {
  ret "document.title = " + jsQuote(title) + ";";
}