From e7d546b596ccc2f8400f9e6e56a85ce23ff90fb2 Mon Sep 17 00:00:00 2001
From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 9 Nov 2021 17:58:36 -0800
Subject: [PATCH] java: Fix building cvc5.jar for cmake 3.16. (#7623)

Fixes #7579.
---
 docs/CMakeLists.txt                               | 1 +
 docs/api/java/CMakeLists.txt                      | 6 ++----
 src/api/cpp/cvc5.h                                | 6 +++---
 src/api/java/CMakeLists.txt                       | 1 -
 src/api/java/io/github/cvc5/api/RoundingMode.java | 6 +++---
 5 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/docs/CMakeLists.txt b/docs/CMakeLists.txt
index f505a7fb4..e37183f90 100644
--- a/docs/CMakeLists.txt
+++ b/docs/CMakeLists.txt
@@ -16,6 +16,7 @@ find_package(Sphinx REQUIRED)
 check_python_module(breathe)
 check_python_module(sphinxcontrib.bibtex sphinxcontrib-bibtex)
 check_python_module(sphinx_tabs.tabs sphinx-tabs)
+check_python_module(sphinxcontrib.programoutput sphinxcontrib.programoutput)
 
 add_subdirectory(api)
 
diff --git a/docs/api/java/CMakeLists.txt b/docs/api/java/CMakeLists.txt
index 7c897a354..54a8dc54c 100644
--- a/docs/api/java/CMakeLists.txt
+++ b/docs/api/java/CMakeLists.txt
@@ -23,11 +23,9 @@ if(BUILD_BINDINGS_JAVA)
   # used to trigger the rebuild
   set(JAVADOC_INDEX_FILE ${JAVADOC_OUTPUT_DIR}/index.html)
 
-  get_target_property(SOURCES cvc5jar SOURCES)
-  
   add_custom_command(
     OUTPUT "${JAVADOC_INDEX_FILE}"
-    COMMAND 
+    COMMAND
       ${Java_JAVADOC_EXECUTABLE} io.github.cvc5.api
       -sourcepath ${CMAKE_SOURCE_DIR}/src/api/java/
       -d ${JAVADOC_OUTPUT_DIR}
@@ -35,7 +33,7 @@ if(BUILD_BINDINGS_JAVA)
       -notimestamp
     COMMAND find ${JAVADOC_OUTPUT_DIR} -type f -exec sed -i'orig' 's/<!-- Generated by javadoc [^>]* -->//' {} "\;"
     COMMAND find ${SPHINX_GH_OUTPUT_DIR} -name '*orig' -delete
-    DEPENDS cvc5jar ${SOURCES}
+    DEPENDS cvc5jar
     COMMENT "Generating javadocs"
   )
 
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 5b0cc0b45..91a6ae447 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -2648,19 +2648,19 @@ enum RoundingMode
   ROUND_NEAREST_TIES_TO_EVEN,
   /**
    * Round towards positive infinity (+oo).
-   * The result shall be the format’s floating-point number (possibly +oo)
+   * The result shall be the format's floating-point number (possibly +oo)
    * closest to and no less than the infinitely precise result.
    */
   ROUND_TOWARD_POSITIVE,
   /**
    * Round towards negative infinity (-oo).
-   * The result shall be the format’s floating-point number (possibly -oo)
+   * The result shall be the format's floating-point number (possibly -oo)
    * closest to and no less than the infinitely precise result.
    */
   ROUND_TOWARD_NEGATIVE,
   /**
    * Round towards zero.
-   * The result shall be the format’s floating-point number closest to and no
+   * The result shall be the format's floating-point number closest to and no
    * greater in magnitude than the infinitely precise result.
    */
   ROUND_TOWARD_ZERO,
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index 58f9ee4b5..ecfec2109 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -140,6 +140,5 @@ add_jar(cvc5jar
   VERSION ${CVC5_VERSION}
   OUTPUT_NAME cvc5
 )
-set_target_properties(cvc5jar PROPERTIES SOURCES "${JAVA_FILES}")
 
 add_dependencies(cvc5jar generate-java-kinds cvc5jni cvc5)
diff --git a/src/api/java/io/github/cvc5/api/RoundingMode.java b/src/api/java/io/github/cvc5/api/RoundingMode.java
index ecc01c342..6a3c274a1 100644
--- a/src/api/java/io/github/cvc5/api/RoundingMode.java
+++ b/src/api/java/io/github/cvc5/api/RoundingMode.java
@@ -25,19 +25,19 @@ public enum RoundingMode {
   ROUND_NEAREST_TIES_TO_EVEN(0),
   /**
    * Round towards positive infinity (+oo).
-   * The result shall be the format’s floating-point number (possibly +oo)
+   * The result shall be the format's floating-point number (possibly +oo)
    * closest to and no less than the infinitely precise result.
    */
   ROUND_TOWARD_POSITIVE(1),
   /**
    * Round towards negative infinity (-oo).
-   * The result shall be the format’s floating-point number (possibly -oo)
+   * The result shall be the format's floating-point number (possibly -oo)
    * closest to and no less than the infinitely precise result.
    */
   ROUND_TOWARD_NEGATIVE(2),
   /**
    * Round towards zero.
-   * The result shall be the format’s floating-point number closest to and no
+   * The result shall be the format's floating-point number closest to and no
    * greater in magnitude than the infinitely precise result.
    */
   ROUND_TOWARD_ZERO(3),
-- 
2.30.2