diff --git a/Misc/build.sh b/Misc/build.sh index 423e96de080..43b3ce44151 100755 --- a/Misc/build.sh +++ b/Misc/build.sh @@ -263,7 +263,7 @@ if [ $conflict_count != 0 ]; then echo "Conflict detected in $CONFLICTED_FILE. Doc build skipped." > ../build/$F err=1 else - make update html >& ../build/$F + make checkout update html >& ../build/$F err=$? fi update_status "Making doc" "$F" $start