<!--
//
// format date as dd-mmm-yy
// example: 12-Jan-99
//
function date_yyyymmmdd(date)
{
  var d = date.getDate();
  var m = date.getMonth() + 1;
  var y = date.getFullYear(); // getYear();   // handle different year values
  // returned by IE and NS in
  // the year 2000.
  var mmm =
    ( 1==m)?'Jan':( 2==m)?'Feb':(3==m)?'Mar':
    ( 4==m)?'Apr':( 5==m)?'May':(6==m)?'Jun':
    ( 7==m)?'Jul':( 8==m)?'Aug':(9==m)?'Sep':
    (10==m)?'Oct':(11==m)?'Nov':'Dec';
  return "" + mmm + " " + d + ", " + y;
}

//
// get last modified date of the
// current document.
//
function date_lastmodified()
{
  var lmd = document.lastModified;
  var s   = "Unknown";
  var d1;   // check if we have a valid date
  // before proceeding
  if(0 != (d1=Date.parse(lmd)))
  {
    s = "" + date_yyyymmmdd(new Date(d1));
  }
  return lmd.slice(0,15);
}

function html_validate()
{
    return "<a href=\"http://validator.w3.org/check/referer\">" +
	"<img border=\"0\" src=\"http://www.w3.org/Icons/valid-html401\"" +
	"alt=\"Valid HTML 4.01!\" height=\"31\" width=\"88\"></a>";
}

function css_validate()
{
    return "<a href=\"http://jigsaw.w3.org/css-validator/\">" +
	"<img border=\"0\" src=\"http://jigsaw.w3.org/css-validator/images/vcss\"" +
	"alt=\"Valid CSS!\"></a>";
}

//
// finally display the last modified date
// as YYYY MMM DD
//
document.write(
	       "<table width=\"100%\" border=\"0\"><tr><td class=\"bgtext\">" +
	       "This page was updated on " +
	       date_lastmodified() +
	       "<br><a href=\"mailto:pede\@daimi.au.dk\">pede\@daimi.au.dk</a>" +
	       "</td><td class=\"bgtext\" align=\"right\">" +
	       html_validate() + "&nbsp;&nbsp;" + css_validate() + 
	       "</td></tr></table>");

// -->
