diff --git a/Dockerfile b/Dockerfile index 38039390b..0bd9b713d 100644 --- a/Dockerfile +++ b/Dockerfile @@ -7,6 +7,8 @@ RUN apt-get -y update \ && apt-get -y install libgmp-dev \ && apt-get -y install libmpfr-dev \ && apt-get -y install libmpc-dev \ + # For krb5-user installation + && export DEBIAN_FRONTEND=noninteractive \ && apt-get -y install krb5-user \ && rm -rf /var/lib/apt/lists/*