diff options
| -rwxr-xr-x | scripts/ci-run.sh | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/scripts/ci-run.sh b/scripts/ci-run.sh index d02f7b52e..b0ebfd894 100755 --- a/scripts/ci-run.sh +++ b/scripts/ci-run.sh @@ -308,10 +308,7 @@ build () { #--- make gstart "[GHDL - build] Make" - set +e - make LIB_CFLAGS="$LIB_CFLAGS" OPT_FLAGS="$OPT_FLAGS" -j`nproc` 2>make_err.log - tail -1000 make_err.log - set -e + make LIB_CFLAGS="$LIB_CFLAGS" OPT_FLAGS="$OPT_FLAGS" -j"$(nproc)" gend gstart "[GHDL - build] Install" |