diff options
Diffstat (limited to '.circleci/prepare-system.sh')
| -rwxr-xr-x | .circleci/prepare-system.sh | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/.circleci/prepare-system.sh b/.circleci/prepare-system.sh index d42424372a..804e0fd890 100755 --- a/.circleci/prepare-system.sh +++ b/.circleci/prepare-system.sh @@ -12,6 +12,7 @@ hackage_index_state="@1522046735" 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 cat > mk/build.mk <<EOF V=1 @@ -24,6 +25,13 @@ BeConservative=YES INTEGER_LIBRARY=$INTEGER_LIBRARY EOF +cat <<EOF >> mk/build.mk +BuildFlavour=$BUILD_FLAVOUR +ifneq "\$(BuildFlavour)" "" +include mk/flavours/\$(BuildFlavour).mk +endif +EOF + case "$(uname)" in Linux) if [[ -n ${TARGET:-} ]]; then |