diff options
Diffstat (limited to 'scripts/build/run-tests.sh')
| -rwxr-xr-x | scripts/build/run-tests.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/scripts/build/run-tests.sh b/scripts/build/run-tests.sh index 32f9a74f..bcd7ce2b 100755 --- a/scripts/build/run-tests.sh +++ b/scripts/build/run-tests.sh @@ -95,7 +95,7 @@ function upload_coverage() { } function run_docker() { - docker_arguments=(docker run -u root --cap-add SYS_PTRACE -ti) + docker_arguments=(docker run -u root --cap-add SYS_PTRACE -t) script_arguments=("--debug" '"/tmp/klee_build"*') if [[ "${COVERAGE}" -eq 1 ]]; then script_arguments+=("--coverage") |