Fixed a link in the navigation menu system pointing to a non-existent pdf file. Only reason I'm posting is because it took a few minutes to work through the javascript files used to implement the navigation and find the right file.

All the pages share common files for the navigation menus. Those files
are in the "script_files" folder. The submenus are each in their own files named "menu1.js", "menu2.js" etc. The submenu filename is used by javascript mouseevents on the top level navigation items, so I don't know if the number is just arbitrary or is actually used as an integer anywhere in the code handling the menus.