diff --git a/build b/build index 1850c17583c21a41a102533f698f2cec6db715c6..ddc887dbf69bb6d8d29e7d9715087067ef24645b 100755 --- a/build +++ b/build @@ -299,7 +299,7 @@ if ! $make -C "$BUILD_DIR" ${VERBOSE} $make_target; then fi if [[ ${BUILD_DOC} == "yes" ]]; then - "$ROOT_DIR/Documentation/build" --prefix="$PREFIX" + "$ROOT_DIR/Documentation/build" --prefix="$PREFIX" --install="$INSTALL" fi if [[ ${BUILD_TESTS} == "yes" ]] || [[ ${BUILD_MATRIX_TESTS} == "yes" ]]; then