//
// format date
//
function date_lastmodified()
{
  var lmd = document.lastModified;
  var s   = "Unknown";
  var d;

  // check if we have a valid date before proceeding
  if (0 != (d=Date.parse(lmd))) {
    s = "" + (new Date(d)).toGMTString();
  }
  return s;
}


document.write(
  "<table width=\"100%\">\
     <tr>\
       <td align=left class=footer>\
         Maintained by Axel Riese &#149;\
         [<A HREF=\"mailto:Axel.Riese@risc.uni-linz.ac.at\">Contact</A>] &#149;\
         [<A HREF=\"/people/ariese\">Home</A>]\
       </td>\
       <td align=right class=footer>\
         Last modified on " + date_lastmodified() + "\
       </td>\
     </tr>\
   </table>")