| changeset 8070 | dbbef2367723 |
| parent 8056 | 3c587e7b8fe5 |
| child 9285 | 21bfc8c14c3d |
--- a/Admin/page/main-layout/navigation.html Tue Dec 21 15:03:02 1999 +0100 +++ b/Admin/page/main-layout/navigation.html Wed Dec 22 16:12:38 1999 +0100 @@ -9,7 +9,7 @@ <!-- _GP_ setnavcolor("#F0F0F0") --> <!-- _GP_ page("Home", "index") --> <!-- _GP_ empty_line(3) --> -<!-- _GP_ page("About", "about") --> +<!-- _GP_ page("Isabelle?", "about") --> <!-- _GP_ empty_line(3) --> <!-- _GP_ page("Documentation", "docs") --> <!-- _GP_ empty_line(3) -->