Skip to content
Snippets Groups Projects

Print execution statistics at the end of execution

Merged Stéphane Del Pino requested to merge feature/exec-stats into develop
11 files
+ 241
12
Compare changes
  • Side-by-side
  • Inline

Files

+ 13
1
@@ -97,7 +97,19 @@ if (EMACS AND GNUPLOT_FOUND AND GMSH)
COMMENT "Building user documentation in doc/userdoc.pdf"
VERBATIM)
add_custom_target(userdoc-pdf DEPENDS pugsdoc-dir "${PUGS_BINARY_DIR}/doc/userdoc.pdf" )
configure_file("${PUGS_SOURCE_DIR}/doc/build-userdoc-pdf.sh.in"
"${PUGS_BINARY_DIR}/doc/build-userdoc-pdf.sh"
FILE_PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE
@ONLY)
set_source_files_properties(
${PUGS_BINARY_DIR}/build-pdf.sh2
PROPERTIES
GENERATED TRUE
HEADER_FILE_ONLY TRUE
)
add_custom_target(userdoc-pdf DEPENDS pugsdoc-dir "${PUGS_BINARY_DIR}/doc/userdoc.pdf" "${PUGS_BINARY_DIR}/doc/build-userdoc-pdf.sh")
add_dependencies(userdoc userdoc-pdf)
Loading