/* lastModification.js
   just prints the date of the last modification of the file
   in the right lower edge of the document. */

document.write("<br><div align='right' style='font-size:60%'>");
document.write("Letzte &#196;nderung: " + document.lastModified );
document.write("</div>");