proxy settings

[anton-malakhov]

I had hard times configuring Docker for corporate proxy. It looks like there is just no way to do it externally w.r.t. your Dockerfile, so I had to modify it with the following patch:

diff --git a/Dockerfile b/Dockerfile
index c9a3022..e8a95ef 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -1,6 +1,9 @@
 FROM ubuntu:16.04
 MAINTAINER [email protected]
-
+ARG http_proxy
+ENV http_proxy=$http_proxy
+ARG https_proxy
+ENV https_proxy=$https_proxy
 RUN DEBIAN_FRONTEND=noninteractive \
         apt-get update && apt-get install -y \
             language-pack-en
diff --git a/build.sh b/build.sh
index 8e128c7..88957b9 100755
--- a/build.sh
+++ b/build.sh
@@ -1,3 +1,3 @@
 #!/bin/bash

-docker build -t magic/benchmark $(dirname $0)
+docker build --build-arg http_proxy="$http_proxy" --build-arg https_proxy="$https_proxy"  -t magic/benchmark $(dirname $0)