equal
deleted
inserted
replaced
28 *) |
28 *) |
29 EOF |
29 EOF |
30 |
30 |
31 for FILE in $INTERMEDIATE_FILES |
31 for FILE in $INTERMEDIATE_FILES |
32 do |
32 do |
33 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' -e 's/Unsafe\.(.*)/\1/g;' $FILE |
33 perl -p -e 's/\bref\b/Unsynchronized.ref/g;' \ |
|
34 -e 's/Unsafe\.(.*)/\1/g;' \ |
|
35 -e 's/\b(Char\.ord\()CharVector\.sub\b/\1String\.sub/g;' $FILE |
34 done |
36 done |
35 ) > tptp_lexyacc.ML |
37 ) > tptp_lexyacc.ML |
36 |
38 |
37 rm -f $INTERMEDIATE_FILES tptp.yacc.desc |
39 rm -f $INTERMEDIATE_FILES tptp.yacc.desc |