sS hjs_setTitleStatus() {
  ret hjs([[
    var originalWindowTitle;
    var lastTitleStatus = "";
    
    window.setTitleStatus = function(status) {
      if (originalWindowTitle == null)
        originalWindowTitle = document.title;
      if (status) status = status + " ";
      if (status != lastTitleStatus) {
        lastTitleStatus = status;
        document.title = status + originalWindowTitle;
      }
    };
    
    window.resetTitle = function() {
      window.setTitleStatus("");
    };
  ]]);
}