From 6c69788264be9e4ba8c5161018061e3e21e9ad14 Mon Sep 17 00:00:00 2001 From: Jonathan Protzenko Date: Wed, 5 May 2021 11:31:02 -0700 Subject: [PATCH] fix --- .docker/build/build.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.docker/build/build.sh b/.docker/build/build.sh index a413892de..db1557498 100644 --- a/.docker/build/build.sh +++ b/.docker/build/build.sh @@ -139,7 +139,7 @@ function exec_build() { # this is a special file that is parsed by Azure Devops result_file="../result.txt" - if misc && check_version_controlled && make clean && make -j $threads && \ + if misc && check_version_controlled && make -C kremlib clean && make -j $threads && \ make -C test everything -j $threads && \ make -C book/tutorial && \ refresh_tutorial