chore: fix foreign test on macOS, again

leanprover · Nov 9, 2021 · 2d14517 · 2d14517
1 parent 1d5c478
commit 2d14517
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
@@ -81,7 +81,8 @@ ENDFOREACH(T)
 
 add_test(NAME leancomptest_foreign
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/compiler/foreign"
-         COMMAND bash -c "${LEAN_BIN}/leanmake --always-make CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'")
+         # LEANC_OPTS is necessary for macOS c++ to find its headers, GMP will be remove soon
+         COMMAND bash -c "${LEAN_BIN}/leanmake --always-make CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS} -L ${GMP_INSTALL_PREFIX}'")
 add_test(NAME leancomptest_doc_example
          WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler"
          COMMAND bash -c "export ${TEST_VARS}; leanmake --always-make bin && ./build/bin/test hello world")