diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-04-22 21:27:54 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-22 19:27:54 +0000 |
| commit | 0869a09f1161480de24c412b12954fc84943bab2 (patch) | |
| tree | a59a629ade76b3c739280b38123f07c916592f91 /src/api/cpp/cvc5.cpp | |
| parent | 7295b8da3f77d0121ab0215a7f309dab90b02854 (diff) | |
Remove unused stuff from options setup (#6422)
This PR removes some old stuff from our options setup that has not been used in a long time.
Most prominently, this includes the man pages that were still generated, and the alias and links options, which no longer worked anyway.
Diffstat (limited to 'src/api/cpp/cvc5.cpp')
0 files changed, 0 insertions, 0 deletions