static S hjs_reloadWindowIn(double seconds) {
  ret hjavascript("setTimeout(function() { window.location.reload(); }, " + toMS(seconds) + ");");
}