From fd96a6e2cf6f87388bcf1101ed8f35da8fe5be43 Mon Sep 17 00:00:00 2001
From: Michiel Borkent <michielborkent@gmail.com>
Date: Fri, 24 Apr 2020 17:44:45 +0200
Subject: [PATCH] Fix Github docker

---
 .github/script/docker | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/script/docker b/.github/script/docker
index a0121d94..f5d2bffc 100755
--- a/.github/script/docker
+++ b/.github/script/docker
@@ -19,7 +19,7 @@ if [ -z "$GITHUB_HEAD_REF" ] && [ "${GITHUB_REF##*/}" = "master" ]
 then
     echo "Building Docker image $image_name:$image_tag"
     echo "$DOCKERHUB_PASS" | docker login -u "$DOCKERHUB_USER" --password-stdin
-    docker build -t "$image_name" .
+    docker build -t "$image_name" --build-arg BABASHKA_XMX="-J-Xmx6300m" .
     docker tag "$image_name:$latest_tag" "$image_name:$image_tag"
     # we only update latest when it's not a SNAPSHOT version
     if [ "false" = "$snapshot" ]; then