# HG changeset patch
# User Edouard Tisserant <edouard.tisserant@gmail.com>
# Date 1652977163 -7200
# Node ID c460ec8c65e9332894e1569db3a581f6be2ee466
# Parent  1a2658f109da9e7940199ccbac9a21e0f411a5eb
Don't require TTY for docker.

diff -r 1a2658f109da -r c460ec8c65e9 Dockerfile
--- a/Dockerfile	Thu May 19 18:08:47 2022 +0200
+++ b/Dockerfile	Thu May 19 18:19:23 2022 +0200
@@ -18,11 +18,13 @@
 ARG GID=1000
 RUN groupadd -g $GID $UNAME
 RUN useradd -m -u $UID -g $GID -s /bin/bash $UNAME
-USER $UNAME
-
-RUN mkdir /home/$UNAME/build /home/$UNAME/src
 
 # easy to remember 'build' alias to invoke main makefile
 ARG OWNDIRBASENAME=beremiz_public_dist
 ENV OWNDIRBASENAME ${OWNDIRBASENAME}
-RUN echo "alias build='make -C /home/"$UNAME"/build -f /home/devel/src/"$OWNDIRBASENAME"/Makefile'">/home/$UNAME/.bash_aliases
+RUN echo -e '#!/bin/bash\nmake -f /home/'$UNAME'/src/'$OWNDIRBASENAME'/Makefile $*' > /usr/local/bin/build
+RUN chmod +x /usr/local/bin/build
+
+USER $UNAME
+
+RUN mkdir /home/$UNAME/build /home/$UNAME/src
diff -r 1a2658f109da -r c460ec8c65e9 build_in_docker.sh
--- a/build_in_docker.sh	Thu May 19 18:08:47 2022 +0200
+++ b/build_in_docker.sh	Thu May 19 18:19:23 2022 +0200
@@ -3,6 +3,6 @@
 CONTAINER=beremiz_public_builder_current
 
 docker start $CONTAINER 
-docker exec -i -t $CONTAINER bash -i -c build $1
+docker exec $CONTAINER bash -c build $1
 docker stop $CONTAINER