diff --git a/demos/nov-2023/Makefile b/demos/nov-2023/Makefile index 0ae0f907..9ddde3ad 100644 --- a/demos/nov-2023/Makefile +++ b/demos/nov-2023/Makefile @@ -5,7 +5,12 @@ ifdef json endif ifdef docker - PATE=docker run --rm -it -v .:/work --workdir=/work pate $(JSON_FLAG) + ifdef json + # Don't run with terminal when using json interface + PATE=docker run --rm -i -v .:/work --workdir=/work pate $(JSON_FLAG) + else + PATE=docker run --rm -it -v .:/work --workdir=/work pate $(JSON_FLAG) + endif else PATE=../../pate.sh $(JSON_FLAG) endif