var lastmodified_oldonload = window.onload;
window.onload = function() {
	var lm = document.createTextNode("Last modified " + document.lastModified + ".");
	var e = document.getElementById("lastmodified");
	if (e != null) {
		e.appendChild(lm);
	}
	if (lastmodified_oldonload != null) {
		lastmodified_oldonload();
	}
}