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 b08a5d4..94b496d 100755 --- a/Misc/build.sh +++ b/Misc/build.sh @@ -231,7 +231,7 @@ if [ $conflict_count != 0 ]; then echo "Conflict detected in $CONFLICTED_FILE. Doc build skipped." > ../build/$F err=1 else - make html >& ../build/$F + make update html >& ../build/$F err=$? fi update_status "Making doc" "$F" $start |