diff options
| -rwxr-xr-x | Misc/build.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Misc/build.sh b/Misc/build.sh index 8a15b0d65a..2c09fbb481 100755 --- a/Misc/build.sh +++ b/Misc/build.sh @@ -266,7 +266,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 |