diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-16 17:12:03 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-16 15:12:03 +0000 |
| commit | 353006984c0c7bbd1bd419c04e4bb873c7eee52a (patch) | |
| tree | d82c08a7f2cc8c4bd6ea5899ebb1829124a36503 /src/parser/tptp/Tptp.g | |
| parent | 6203bcb456d5450770c8ac6cdb775ec0f73e0325 (diff) | |
Fix dependencies for stats options (#6378)
A last-minute edit in a previous PR broke the handling of dependencies between the statistic options.
Diffstat (limited to 'src/parser/tptp/Tptp.g')
0 files changed, 0 insertions, 0 deletions