document.write("<DIV CLASS='bunntekst'>");
document.write("<A HREF='#topp'>~</A>");
document.write("<A HREF='http://www.cs.cmu.edu/~jinghai' NAME='bunn'>Jinghai Rao 20&copy;03</A><br>");
if (Date.parse(document.lastModified) != 0) {
    var modiDate = new Date(document.lastModified);
    var modiMonth = modiDate.getMonth()+1;
    var modiYear = modiDate.getYear()+1900;
    document.write("Last modified: " + modiDate.getDate() + "/" + modiMonth + "/" + modiYear + ".<br>");
}
document.write("</DIV>");