chore: remove outdated trust0 test (#12401)
This commit is contained in:
parent
df26bea7c1
commit
d29407b481
3 changed files with 0 additions and 18 deletions
|
|
@ -127,18 +127,6 @@ foreach(T ${LEANINTERPTESTS})
|
|||
)
|
||||
endforeach(T)
|
||||
|
||||
# LEAN TESTS using --trust=0
|
||||
file(GLOB LEANT0TESTS "${LEAN_SOURCE_DIR}/../tests/lean/trust0/*.lean")
|
||||
foreach(T ${LEANT0TESTS})
|
||||
get_filename_component(T_NAME ${T} NAME)
|
||||
cmake_path(RELATIVE_PATH T BASE_DIRECTORY ${LEAN_SOURCE_DIR}/.. OUTPUT_VARIABLE T_PATH)
|
||||
add_test(
|
||||
NAME "${T_PATH}"
|
||||
WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/trust0"
|
||||
COMMAND bash -c "${TEST_VARS} ./test_single.sh ${T_NAME}"
|
||||
)
|
||||
endforeach(T)
|
||||
|
||||
# LEAN PACKAGE TESTS
|
||||
file(GLOB LEANPKGTESTS "${LEAN_SOURCE_DIR}/../tests/pkg/*")
|
||||
foreach(T ${LEANPKGTESTS})
|
||||
|
|
|
|||
|
|
@ -1,2 +0,0 @@
|
|||
import Init.System.IO
|
||||
-- #print trust
|
||||
|
|
@ -1,4 +0,0 @@
|
|||
#!/usr/bin/env bash
|
||||
source ../../common.sh
|
||||
|
||||
exec_check_raw lean -t0 -Dlinter.all=false "$f"
|
||||
Loading…
Add table
Reference in a new issue