fix

FStarLang · May 5, 2021 · 6c69788 · 6c69788
1 parent a5523d8
commit 6c69788
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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