From 81c0ec2126d5cb7256a7dc0adb0137adeaf4bb6b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jakub=20Klinkovsk=C3=BD?= <klinkovsky@mmg.fjfi.cvut.cz>
Date: Fri, 15 Oct 2021 20:46:04 +0200
Subject: [PATCH] build script: added missing parameter to install the
documentation
---
build | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/build b/build
index 1850c17583..ddc887dbf6 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
--
GitLab