max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: fix Lake rename

Browse source
This commit is contained in:
Sebastian Ullrich 2022-11-28 15:12:18 +01:00
parent c4ff5fe199
commit c112ae7c58
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/shell/CMakeLists.txt
View file

@ -173,7 +173,7 @@ ENDFOREACH(T)
# Create a lake test for each subdirectory of `lake/examples` which contains a `test.sh` file.
file(GLOB_RECURSE LEANLAKETESTS "${LEAN_SOURCE_DIR}/lake/examples/test.sh")
FOREACH(T ${LEANLAKETESTS})
if(NOT T MATCHES ".*lean_packages.*")
if(NOT T MATCHES ".*lake-packages.*")
if(NOT T MATCHES ".*bootstrap.*")
GET_FILENAME_COMPONENT(T_DIR ${T} DIRECTORY)
GET_FILENAME_COMPONENT(DIR_NAME ${T_DIR} NAME)