--- a/Admin/page/index.html Mon Nov 02 21:36:48 1998 +0100 +++ b/Admin/page/index.html Mon Nov 02 21:57:49 1998 +0100 @@ -1,7 +1,7 @@ <html> <head> -<-- $Id$ --> +<!-- $Id$ --> <title>Isabelle</title> <body>