From 77ccd92963a57dd6002501fc4591852937e1a08b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 17 Nov 2021 09:32:53 +0100
Subject: [PATCH] chore: remove redundant cmake `install` directive

---
 src/CMakeLists.txt | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index aa2d30f358..03d36daca0 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -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"