diff --git a/tools/ci-build b/tools/ci-build index e813bd98a..f618a2da5 100755 --- a/tools/ci-build +++ b/tools/ci-build @@ -74,7 +74,7 @@ done make=make instdir="$HOME/ocaml-tmp-install" workdir=. -checkout=false +docheckout=false nt= case "$arch" in