diff --git a/src/stdlib.make.in b/src/stdlib.make.in index e6f96cbe94..87a4edb28e 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -10,7 +10,7 @@ LEANMAKE_OPTS=\ BIN_OUT="${CMAKE_BINARY_DIR}/bin"\ LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\ LEANC_OPTS+="${LEANC_OPTS}"\ - LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}" + LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\ MORE_DEPS+="${PREV_STAGE}/bin/lean${CMAKE_EXECUTABLE_SUFFIX}"\ CMAKE_LIKE_OUTPUT=1