docTitle = "";
page = top.location.href;

if (page.lastIndexOf("index.html") == -1 && page.lastIndexOf("/") != page.length - 1) {
  page = page.substring(page.lastIndexOf("/") + 1, page.lastIndexOf("."));
  top.location.href = "../index.html?" + page;
}

function setTabTitle(title) {
  docTitle = title;
  updateTitle();
}

function updateTitle() {
  if (parent.tabFrame.document.getElementById("title")) {
    parent.tabFrame.document.getElementById("title").innerHTML = docTitle;
  } else {
    setTimeout("updateTitle()", 500);
  }
}