Fix CI

protz · protz · commit cd04835f7a8d · 2021-05-05T11:24:59.000-07:00
diff --git a/.docker/build/build.sh b/.docker/build/build.sh
@@ -131,7 +131,6 @@ function refresh_tutorial() {
 }
 
 function check_version_controlled() {
-  make -C kremlib clean && \
   make -C kremlib/dist/generic -f Makefile.basic -j
 }
 
@@ -140,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 -j $threads && \
+    if misc && check_version_controlled && make clean && make -j $threads && \
       make -C test everything -j $threads && \
       make -C book/tutorial && \
       refresh_tutorial

Original file line number	Diff line number	Diff line change
`@@ -131,7 +131,6 @@ function refresh_tutorial() {`
`131`	`131`	`}`
`132`	`132`
`133`	`133`	`function check_version_controlled() {`
`134`		`- make -C kremlib clean && \`
`135`	`134`	`make -C kremlib/dist/generic -f Makefile.basic -j`
`136`	`135`	`}`
`137`	`136`
`@@ -140,7 +139,7 @@ function exec_build() {`
`140`	`139`	`# this is a special file that is parsed by Azure Devops`
`141`	`140`	`result_file="../result.txt"`
`142`	`141`
`143`		`- if misc && check_version_controlled && make -j $threads && \`
	`142`	`+ if misc && check_version_controlled && make clean && make -j $threads && \`
`144`	`143`	`make -C test everything -j $threads && \`
`145`	`144`	`make -C book/tutorial && \`
`146`	`145`	`refresh_tutorial`