/* Updated.js
 *
 * Inserts a 'last updated' message into the current page.
 */

d = new Date(document.lastModified);
m = d.getMonth();
if(m==0) mo=" Jan ";
if(m==1) mo=" Feb ";
if(m==2) mo=" Mar ";
if(m==3) mo=" Apr ";
if(m==4) mo=" May ";
if(m==5) mo=" Jun ";
if(m==6) mo=" Jul ";
if(m==7) mo=" Aug ";
if(m==8) mo=" Sep ";
if(m==9) mo=" Oct ";
if(m==10) mo=" Nov ";
if(m==11) mo=" Dec ";

y = d.getYear();
if( y < 2000 ) {
	if( y < 100 ) {
		y += 2000;
	} else {
		y += 1900;
	}
}

document.write('--- Last updated ' + d.getDate() + mo + y + ' ---');