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