Is using a point in a filename okay? Some years ago this could cause some troubles (at least in Windows). Maybe we should use another time format for filenames instead?