diff options
Diffstat (limited to 'docker')
| -rw-r--r-- | docker/Dockerfile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docker/Dockerfile b/docker/Dockerfile index 6d73d9b2..14973dfd 100644 --- a/docker/Dockerfile +++ b/docker/Dockerfile @@ -499,7 +499,7 @@ RUN echo "$(opam env --root=/opt/opam --set-root)" >> /etc/skel/.bashrc && \ RUN rm -rf /tmp/* # Disable mouse in vim -RUN echo -e "set mouse=\nset ttymouse=" > /etc/vim/vimrc.local +RUN printf "set mouse=\nset ttymouse=\n" > /etc/vim/vimrc.local COPY entrypoint.sh /usr/local/bin/entrypoint.sh |