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