projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 4bba39f) | patch
Improve error message for missing options include (#8154)
authorGereon Kremer <gkremer@cs.stanford.edu>
Thu, 24 Feb 2022 20:17:45 +0000 (21:17 +0100)
committerGitHub <noreply@github.com>
Thu, 24 Feb 2022 20:17:45 +0000 (20:17 +0000)
commit2481c6194dc1d9d35562cbf18fdfc572961997d6
tree02d600279608b2fba89920f29d704c88f77858c4tree
parent4bba39f1b52210c7a31b8e7542df9dc15b9700c1commit | diff
Improve error message for missing options include (#8154)

This PR improves the error message if one tries to use options whose header have not been included.
src/options/mkoptions.py diff | blob | history