diff -r 4fe5d5aff4df -r 9ef3db99f24a Admin/page/index.html --- 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 @@ +<-- $Id$ --> Isabelle