chore: fix foreign test on macOS
This commit is contained in:
parent
b053679d6d
commit
a345a98ef7
2 changed files with 2 additions and 1 deletions
1
.github/workflows/ci.yml
vendored
1
.github/workflows/ci.yml
vendored
|
|
@ -133,6 +133,7 @@ jobs:
|
|||
if: matrix.name == 'macOS'
|
||||
run: |
|
||||
cd build/stage1
|
||||
cp /usr/local/opt/gmp/lib/libgmp.* lib/
|
||||
for f in lib/lean/libleanshared.dylib bin/lean bin/leanpkg bin/leanc bin/lake; do
|
||||
for lib in $(otool -L $f | tail -n +2 | cut -d' ' -f1); do
|
||||
# copy Homebrew dependencies
|
||||
|
|
|
|||
|
|
@ -79,7 +79,7 @@ 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}")
|
||||
COMMAND bash -c "${LEAN_BIN}/leanmake --always-make CXX='${CMAKE_CXX_COMPILER} ${LEANC_OPTS}'")
|
||||
add_test(NAME leancomptest_doc_example
|
||||
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../doc/examples/compiler"
|
||||
COMMAND bash -c "${LEAN_BIN}/leanmake --always-make bin && ./build/bin/test hello world")
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue