Merge branch 'master' of github.com:google/or-tools

wen-zheng · Jun 12, 2020 · 45770b8 · 45770b8
2 parents 75403ab + de9cc58
commit 45770b8
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/tools/docker/ubuntu-20.04.Dockerfile b/tools/docker/ubuntu-20.04.Dockerfile
@@ -6,7 +6,7 @@ FROM ubuntu:20.04 AS env
 ##  SETUP  ##
 #############
 RUN apt update -qq \
-&& apt install -yq \
+&& DEBIAN_FRONTEND=noninteractive apt install -yq \
  git pkg-config wget make cmake autoconf libtool zlib1g-dev gawk g++ curl subversion \
  lsb-release \
 && apt clean \