diff options
Diffstat (limited to 'tools/ci.sh')
| -rwxr-xr-x | tools/ci.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/ci.sh b/tools/ci.sh index e8c4021f37..8d361e2b39 100755 --- a/tools/ci.sh +++ b/tools/ci.sh @@ -395,14 +395,14 @@ function ci_teensy_build { CI_UNIX_OPTS_SYS_SETTRACE=( MICROPY_PY_BTREE=0 MICROPY_PY_FFI=0 - MICROPY_PY_USSL=0 + MICROPY_PY_SSL=0 CFLAGS_EXTRA="-DMICROPY_PY_SYS_SETTRACE=1" ) CI_UNIX_OPTS_SYS_SETTRACE_STACKLESS=( MICROPY_PY_BTREE=0 MICROPY_PY_FFI=0 - MICROPY_PY_USSL=0 + MICROPY_PY_SSL=0 CFLAGS_EXTRA="-DMICROPY_STACKLESS=1 -DMICROPY_STACKLESS_STRICT=1 -DMICROPY_PY_SYS_SETTRACE=1" ) |