Remove redundant options headers from TPTP parser. (#8864)
authorMathias Preiner <mathias.preiner@gmail.com>
Tue, 7 Jun 2022 18:06:37 +0000 (11:06 -0700)
committerGitHub <noreply@github.com>
Tue, 7 Jun 2022 18:06:37 +0000 (18:06 +0000)
commit129f72e42965992e208dba89cebd5582a9ee04f3
tree34591814b4334f67ae7f4f464a79957b164d9b08
parenta2eab9fb3c82beb531437c05e9f7d354f8858c31
Remove redundant options headers from TPTP parser. (#8864)

Fixes #8861.
src/parser/tptp/tptp.cpp