/* writeMenu * write out the menu on the side bar */ function writeMenu() { document.write( "

", " $\"\"$ ", "Home", "
$\"\"$ ", "Research", "
$\"\"$ ", "Students", "
$\"\"$ ", "Publications", "
$\"\"$ ", "Teaching", "
$\"\"$ ", "Links", "
$\"\"$ ", "Visitor Info", "

" ) }