projects
/
cvc5.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
9b9fef6
)
Remove timestamped javadoc comments (#7304)
author
Gereon Kremer
<nafur42@gmail.com>
Wed, 6 Oct 2021 15:55:55 +0000
(08:55 -0700)
committer
GitHub
<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
patch
|
blob
|
history
diff --git
a/docs/api/java/CMakeLists.txt
b/docs/api/java/CMakeLists.txt
index 6515fc29f1ca08c4ea8fdb63002e141640ec2700..96a5d80b66c380dd98a89ce3245f972d26897d3a 100644
(file)
--- a/
docs/api/java/CMakeLists.txt
+++ b/
docs/api/java/CMakeLists.txt
@@
-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"
)