--- History.py.orig	2008-07-29 00:16:26.000000000 +0200
+++ History.py	2008-07-29 00:15:55.000000000 +0200
@@ -86,7 +86,10 @@
       
       length = file.readline()
       while length:
-         self.history.append(file.read(int(length)))
+         try:
+            self.history.append(file.read(int(length)))
+         except ValueError:
+            print "readline() gaves none int back " + str(length) 
          file.read(1) # This is for \n
          length = file.readline()