function writetitle(text) {
	if (document.all || document.getElementById) {
		top.document.title = text;
	}
}