max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove redundant cmake install directive

Browse source
This commit is contained in:
Sebastian Ullrich 2021-11-17 09:32:53 +01:00
parent abef59ddbb
commit 77ccd92963
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/CMakeLists.txt
View file

@ -524,8 +524,6 @@ add_custom_target(clean-olean
install(DIRECTORY "${CMAKE_BINARY_DIR}/lib/" DESTINATION lib PATTERN temp EXCLUDE)
install(CODE "execute_process(COMMAND sh -c \"cp ${CMAKE_BINARY_DIR}/lib/*.* \${CMAKE_INSTALL_PREFIX}/lib\")")
install(DIRECTORY "${CMAKE_SOURCE_DIR}" DESTINATION lib/lean
FILES_MATCHING
PATTERN "*.lean"