Merge pull request #1323 from davidgyu/dev_ninja_doc_build_fix

Fixed doc build errors when using ninja
This commit is contained in:
David G Yu 2023-09-13 18:38:30 -07:00 committed by GitHub
commit 3ba051c6db
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -269,7 +269,10 @@ if (DOCUTILS_FOUND AND Python_Interpreter_FOUND)
-E copy "${infile}" "${outfile}"
)
add_custom_target( ${src} DEPENDS "${outfile}")
# Exclude generated search.html
if (NOT ${src} STREQUAL "search.html")
add_custom_target( ${src} DEPENDS "${outfile}")
endif()
list(APPEND HTML_TARGETS ${src})