// lastmodified.js
/*
  Write the last modification time of the current document into
  the html

  Use this by including:
  <script language="javascript" src="peter/javascript/lastmodified.js"></script>
  in your html file
*/
document.write("<i>Last modification: "+document.lastModified+"</i>");
// End of lastmodified.js