diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 990bdaf18b..86ed801361 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -555,6 +555,10 @@ configure_file("${LEAN_SOURCE_DIR}/bin/leanc.in" "${CMAKE_BINARY_DIR}/bin/leanc" install(FILES "${CMAKE_BINARY_DIR}/bin/leanc" DESTINATION bin PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE) +file(COPY ${LEAN_SOURCE_DIR}/bin/leanmake DESTINATION ${CMAKE_BINARY_DIR}/bin) +install(FILES ${LEAN_SOURCE_DIR}/bin/leanmake + DESTINATION bin + PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE GROUP_READ GROUP_EXECUTE WORLD_READ WORLD_EXECUTE) # shared library deactivated until we figure out the leanstatic/leanstdlib story # # The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux). diff --git a/src/bin/leanmake b/src/bin/leanmake new file mode 100755 index 0000000000..f2ac1b1c53 --- /dev/null +++ b/src/bin/leanmake @@ -0,0 +1,5 @@ +#!/usr/bin/env bash + +set -euo pipefail +bindir=$(dirname $0) +make -f "$bindir/../share/lean/Makefile" "$@"