//JavaScript functions used to determine the date the html file was last modified as well
//  as format it (dd mmm yyyy)



// format date as dd mmm yyyy (example: 12 Jan 1999)
function FormatDate(date)
  {
  var d = date.getDate();         //day
  var m = date.getMonth() + 1;    //month
  var y = date.getFullYear();         //year
  
  // could use splitString() here but the following method is more compatible
  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 formatted date
  return (d<10?"0"+d:d) +" "+ mmm +" "+ y;
  }//end of FormatDate()
  
function GetDateLastModified()
  {
  var lmd   = document.lastModified;
  var sdate = "Unknown";
  var ddate ;
      
  //check if date is valid before proceeding
  if(0 != (ddate = Date.parse(lmd)))
    {
    sdate = "" + FormatDate(new Date(ddate));
    }//end of if

  return sdate;
  }//end of GetDateLastModified()

//displays the date in the appropriate format
function WriteDateLastModified()
  {
  document.write("Last updated on " + GetDateLastModified());
  }//end of WriteDateLastModified()

WriteDateLastModified();