From 5c409c00a785aec1eb3aacf8879a3a270daace3c Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 5 Jan 2019 15:08:41 +0000 Subject: [PATCH] Disabled SHELL directive. --- debian4isabelle/Dockerfile | 2 +- isabelle/Dockerfile | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/debian4isabelle/Dockerfile b/debian4isabelle/Dockerfile index c475cc7..8229da1 100644 --- a/debian4isabelle/Dockerfile +++ b/debian4isabelle/Dockerfile @@ -26,7 +26,7 @@ FROM debian:testing-slim -SHELL ["/bin/bash", "-c"] +# SHELL ["/bin/bash", "-c"] # packages RUN apt-get -y update && \ diff --git a/isabelle/Dockerfile b/isabelle/Dockerfile index 867d914..fce5e37 100644 --- a/isabelle/Dockerfile +++ b/isabelle/Dockerfile @@ -34,7 +34,7 @@ LABEL isabelle.url="$isabelle" LABEL isabelle.afp.url="$afp" LABEL isabelle.sessions="$sessions" -SHELL ["/bin/bash", "-c"] +# SHELL ["/bin/bash", "-c"] # Create default user (isabelle) RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd)