diff options
Diffstat (limited to '.circleci/prepare-system.sh')
| -rwxr-xr-x | .circleci/prepare-system.sh | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.circleci/prepare-system.sh b/.circleci/prepare-system.sh index 636b792c82..7d8cac60a2 100755 --- a/.circleci/prepare-system.sh +++ b/.circleci/prepare-system.sh @@ -69,6 +69,7 @@ case "$(uname)" in ln -s $HOME/.cabal/bin/alex /usr/local/bin/alex || true ln -s $HOME/.cabal/bin/happy /usr/local/bin/happy || true ln -s $HOME/.cabal/bin/HsColour /usr/local/bin/HsColour || true + echo "libraries/integer-gmp_CONFIGURE_OPTS += --configure-option=--with-intree-gmp" >> mk/build.mk ;; *) fail "uname=$(uname) not supported" |