sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

fix: lake-ci test glob (#12876)

Browse Source 
This PR fixes an error in the test globs for `lake-ci`. With `lake-ci`,
the shake test was created twice, which CMake does not accept.
This commit is contained in:
Mac Malone
2026-03-10 23:31:44 -04:00
committed by GitHub
parent bb047b8725
commit cd85b93d93
1 changed files with 8 additions and 7 deletions
Download Patch File Download Diff File Expand all files Collapse all files

15
tests/CMakeLists.txt
View File

@@ -238,17 +238,18 @@ endforeach(T)
# toolchain: requires elan to download toolchain
# online: downloads remote repositories
option(LAKE_CI "Enable full Lake test suite (use `lake-ci` label on PRs)" OFF)
file(
GLOB_RECURSE LEANLAKETESTS
"${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh"
"${LEAN_SOURCE_DIR}/../tests/lake/tests/shake/test.sh"
)
if(LAKE_CI)
file(
GLOB_RECURSE LEANLAKETESTS_FULL
GLOB_RECURSE LEANLAKETESTS
"${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh"
"${LEAN_SOURCE_DIR}/../tests/lake/tests/test.sh"
)
list(APPEND LEANLAKETESTS ${LEANLAKETESTS_FULL})
else()
file(
GLOB_RECURSE LEANLAKETESTS
"${LEAN_SOURCE_DIR}/../tests/lake/examples/test.sh"
"${LEAN_SOURCE_DIR}/../tests/lake/tests/shake/test.sh"
)
endif()
foreach(T ${LEANLAKETESTS})
if(NOT T MATCHES ".*(lake-packages|bootstrap|toolchain|online).*")