projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7673808) | patch
Add getName() method to options. (#4704)
authorMathias Preiner <mathias.preiner@gmail.com>
Wed, 8 Jul 2020 13:38:26 +0000 (06:38 -0700)
committerGitHub <noreply@github.com>
Wed, 8 Jul 2020 13:38:26 +0000 (08:38 -0500)
commit37801c1da918ad1c4de97e8a64ca7d1177b61de4
tree37f51eb5faa6510e1f61d618323ec22065e7a9b0tree
parent767380812cff0b8299ddf0784c149c80d2e6ecbdcommit | diff
Add getName() method to options. (#4704)

getName() returns the long option name if it exists and an empty string otherwise.
src/options/mkoptions.py diff | blob | history