// We use JavaScript as a way to easily include this header
// information in several HTML pages.

// Menu items
document.write('<table width="100%" border="0" cellspacing="0" cellpadding="0">');
document.write('<tr>');
document.write('<td align="center">');
document.write('<h1>John Mellor-Crummey, Ph.D.</h1>');
document.write('</td>');
document.write('</tr>');
document.write('<tr>');
document.write('<td align="center">');
document.write('[ <a href="index.html">Home</a> |');
document.write('  <a href="research.html">Research</a> |');
document.write('  <a href="teaching.html">Teaching</a> |');
document.write('  Papers (<a href="pubs-year.html">year</a>, ');
document.write('<a href="pubs-area.html">area</a>) |');
document.write('  <a href="affiliations.html">Affiliations</a> ]');
document.write('</td>');
document.write('</tr>');
document.write('</table>');
document.write('<hr>');

// ***************************************************************************