From 3a83b39e95f2dacfdead792ef8cd5c60ff2ef914 Mon Sep 17 00:00:00 2001
From: Felix Krull <f_krull@gmx.de>
Date: Sat, 10 Feb 2018 20:18:49 +0000
Subject: [PATCH] Build Docker images with the other installers.

---
 build-installers.sh | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/build-installers.sh b/build-installers.sh
index 8e07abb3f..92f0d177f 100755
--- a/build-installers.sh
+++ b/build-installers.sh
@@ -136,6 +136,17 @@ mv "Installer/fedora/${RPMNAME}" "${UPDATE_TARGET}"
 echo "Done building rpm package"
 
 
+echo ""
+echo ""
+echo "Building Docker images ..."
+
+cd Installer/Docker
+bash build-images.sh ../../$1
+cd ../..
+
+echo "Done building Docker images"
+
+
 echo ""
 echo ""
 echo "Building Windows instance in virtual machine"