A visitor who stumbles on a page of our site (other than
index.html) will not see the menu, because the menu is on
index.html. To solve this problem, we just put
<script src="no_orphans.js"></script> in the head of the external pages (but we don't put it in
index.html; click on the link to see what must be put inside the js-file).
Note: the links in the other pages are identical (syntactically) to the ones used in
index.html.