projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1409f24) | patch
parsekinds: Remove DEFAULT_HEADER. (#6294)
authorMathias Preiner <mathias.preiner@gmail.com>
Tue, 6 Apr 2021 01:04:11 +0000 (18:04 -0700)
committerGitHub <noreply@github.com>
Tue, 6 Apr 2021 01:04:11 +0000 (18:04 -0700)
commit00a20b53ce998f52b18303a7a680e6a00acc098c
tree2aaf6422fa5c9dc603239a3159cbd079321ca6ddtree
parent1409f24edfcf91698293cc41b43e56a5194b0fdecommit | diff
parsekinds: Remove DEFAULT_HEADER. (#6294)

DEFAULT_HEADER in src/api/parsekinds.py is essentially unused since both genkinds.py scripts pass the kinds header to the script. The current value of DEFAULT_HEADER does not work for the scripts since the working directory for genkinds.py is in src/api/{java,python}.
src/api/java/genkinds.py diff | blob | history
src/api/parsekinds.py diff | blob | history
src/api/python/genkinds.py.in diff | blob | history