def ReadFile(filename):
  file = open(filename, "rt")
  try:
    lines = file.read()
  finally: