diff options
Diffstat (limited to '.ci/ci-make-install.sh')
| -rwxr-xr-x | .ci/ci-make-install.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.ci/ci-make-install.sh b/.ci/ci-make-install.sh index 9b79d8883f..0984b06cb9 100755 --- a/.ci/ci-make-install.sh +++ b/.ci/ci-make-install.sh @@ -5,7 +5,7 @@ set -e if [ "$1" = "release-ready" ] ; then exit 0 fi -travis_fold install "make install" +travis_fold install "ninja install" if [ "$DISTRO" != "" ] ; then docker exec --env EIO_MONITOR_POLL=1 $(cat $HOME/cid) ninja -C build install else |