Skip to content

Commit

Permalink
fix locale settings in our Docker image.
Browse files Browse the repository at this point in the history
Ubuntu 18.04 does not use default locale UTF-8 which causes problems with special chars
(so far only appeared in one case:
https://gitlab.com/sosy-lab/software/cpachecker/-/commit/f166c511babe34d1bc8ed52b7d28d54850732923#note_1420329522).
The collector for ConfigurationOption uses UTF-8 as default, so we also use UTF-8 as default locale.
  • Loading branch information
kfriedberger committed Jun 6, 2023
1 parent 14703b7 commit 6194eba
Showing 1 changed file with 8 additions and 0 deletions.
8 changes: 8 additions & 0 deletions docker/ubuntu1804.Dockerfile
Expand Up @@ -27,6 +27,14 @@ RUN apt-get update \
&& make \
&& make install

# set default locale
RUN apt-get update \
&& apt-get install -y \
locales locales-all
ENV LC_ALL en_US.UTF-8
ENV LANG en_US.UTF-8
ENV LANGUAGE en_US.UTF-8

# Add the user "developer" with UID:1000, GID:1000, home at /developer.
# This allows to map the docker-internal user to the local user 1000:1000 outside of the container.
# This avoids to have new files created with root-rights.
Expand Down

0 comments on commit 6194eba

Please sign in to comment.