var mnths="JanFebMarAprMayJunJulAugSepOctNovDec";
   var update = new Date(document.lastModified);
   dd = update.getDate();
   mm = update.getMonth() * 3;
   ma = mnths.substring(mm,mm+3);
   yy = update.getYear(); yy+=(yy<70)?2000:(yy>1000)?0:1900; document.write("last updated: "+dd+" "+ma+" "+yy+" ");