Remove timestamped javadoc comments (#7304)
authorGereon Kremer <nafur42@gmail.com>
Wed, 6 Oct 2021 15:55:55 +0000 (08:55 -0700)
committerGitHub <noreply@github.com>
Wed, 6 Oct 2021 15:55:55 +0000 (15:55 +0000)
This PR also removes the javadoc timestamps from index.html, which for some reason does not honor the -notimestamp option.

docs/api/java/CMakeLists.txt

index 6515fc29f1ca08c4ea8fdb63002e141640ec2700..96a5d80b66c380dd98a89ce3245f972d26897d3a 100644 (file)
@@ -33,6 +33,8 @@ if(BUILD_BINDINGS_JAVA)
       -d ${JAVADOC_OUTPUT_DIR}
       -cp ${CMAKE_BINARY_DIR}/src/api/java/cvc5.jar
       -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}
     COMMENT "Generating javadocs"
   )