function dateStamp() {
    with( document ) {
	write("<font size=-2>");
	write("(Last updated " + document.lastModified.replace(/ *[0-9]+:[0-9]+:[0-9]+/,"") + ")" );
	write("</font>");
    }
}