changeset 18701 | 98e6a0a011f3 |
parent 18700 | f04a8755d6ca |
child 18702 | 7dc7dcd63224 |
--- a/src/HOL/Tools/ATP/testoutput.py Tue Jan 17 10:26:36 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,24 +0,0 @@ -#!/usr/bin/python - -import string -import sys - -mode = 0 -try: - while 1: - line = sys.stdin.readline() - words = line.split() - if len(words) > 0: - if words[0] == "SPASS": - mode = 1 - if line == '': - break - line = line[:-1] - if mode == 1: - print line -except: - pass -#f.close() - -sys.exit() -