diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2021-03-20 05:23:44 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-20 05:23:44 -0500 |
| commit | a374f7b577b48908d623cf7b64594f1c98cfb8b7 (patch) | |
| tree | 0173b96f4f9ec3c967b3d7d9cf64ed4c1c555d8f /configure.sh | |
| parent | bdc92b3bb257134c01c5e4818e97f71cbb66ab52 (diff) | |
Generate cvc/Kind.java for the java API (#6143)
PR changes:
Refactor python/genkinds.py by separating parsing from file generation.
Add java/genkinds.py to generate file Kind.java.
Enable java API in ./configure.sh with "under development" warning.
Diffstat (limited to 'configure.sh')
| -rwxr-xr-x | configure.sh | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/configure.sh b/configure.sh index ed84a7270..d57bcd5d5 100755 --- a/configure.sh +++ b/configure.sh @@ -295,7 +295,9 @@ do --java-bindings) java_bindings=ON;; --no-java-bindings) java_bindings=OFF;; - --all-bindings) python_bindings=ON;; + --all-bindings) + python_bindings=ON + java_bindings=ON;; --valgrind) valgrind=ON;; --no-valgrind) valgrind=OFF;; |