diff --git a/src/tools/Htmls.hs b/src/tools/Htmls.hs
index dcca7dea6..9732b66c1 100644
--- a/src/tools/Htmls.hs
+++ b/src/tools/Htmls.hs
@@ -4,15 +4,16 @@
-- Stability : (stable)
-- Portability : (portable)
--
--- > CVS $Date: 2005/04/16 05:40:50 $
--- > CVS $Author: peb $
--- > CVS $Revision: 1.5 $
+-- > CVS $Date: 2005/04/16 17:35:42 $
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.6 $
--
-- chop an HTML file into separate files, each linked to the next and previous.
-- the names of the files are n-file, with n = 01,02,...
-- the chopping is performed at each separator, here defined as @\