diff options
Diffstat (limited to '.gitlab')
| -rwxr-xr-x | .gitlab/prepare-system.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/.gitlab/prepare-system.sh b/.gitlab/prepare-system.sh index 56dba70065..a8eabe2678 100755 --- a/.gitlab/prepare-system.sh +++ b/.gitlab/prepare-system.sh @@ -13,6 +13,7 @@ if [[ -z ${BUILD_SPHINX_HTML:-} ]]; then BUILD_SPHINX_HTML=YES; fi if [[ -z ${BUILD_SPHINX_PDF:-} ]]; then BUILD_SPHINX_PDF=YES; fi if [[ -z ${INTEGER_LIBRARY:-} ]]; then INTEGER_LIBRARY=integer-gmp; fi if [[ -z ${BUILD_FLAVOUR:-} ]]; then BUILD_FLAVOUR=perf; fi +if [[ -z ${XZ:-} ]]; then XZ=pxz; fi cat > mk/build.mk <<EOF V=1 @@ -23,7 +24,7 @@ BUILD_SPHINX_HTML=$BUILD_SPHINX_HTML BUILD_SPHINX_PDF=$BUILD_SPHINX_PDF BeConservative=YES INTEGER_LIBRARY=$INTEGER_LIBRARY -XZ_CMD=pxz +XZ_CMD=$XZ EOF cat <<EOF >> mk/build.mk |