diff --git a/scripts/ci-hol4.sh b/scripts/ci-hol4.sh index 5923115aad3ecfbdc033679643f8362699b2b6bd..7853eb1068bc93a69842ba9e8271250d80af564c 100755 --- a/scripts/ci-hol4.sh +++ b/scripts/ci-hol4.sh @@ -38,7 +38,7 @@ FLOVERDIR="$(pwd)" cd ./hol4 -Holmake +Holmake -j1 #cd ./binary