diff --git a/bin/build-src-distrib.sh b/bin/build-src-distrib.sh index 81c5b82053164b80d13ea403f7fe653fd2594e44..fa2215de1f23f42b2fa11fd6144e663006d25fa3 100755 --- a/bin/build-src-distrib.sh +++ b/bin/build-src-distrib.sh @@ -728,7 +728,7 @@ case "${STEP}" in step 1 "COMPILING PDF MANUALS" run "rm -rf $MANUALS_DIR" run "mkdir -p $MANUALS_DIR" - run "$FILTER doc/build-manuals.sh" + run "$FILTER make -C doc all" run "rm -rf $OUT_DIR/manuals" run "mkdir -p $OUT_DIR/manuals" run "cp $MANUALS_DIR/* $OUT_DIR/manuals"