mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-10-03 17:07:41 +03:00
dev-script: fix env variable handling #1673
- change dockerfiles to hardcode environment variables instead of trying to source them from the script - Fix a typo in setting LANG
This commit is contained in:
parent
05392cf94d
commit
36a6f576f6
@ -287,11 +287,11 @@ put_brew_packages_in_path() {
|
||||
set_ubuntu_language_encoding() {
|
||||
case $CRYPTOL_PLATFORM in
|
||||
$UBUNTU20 | $UBUNTU22)
|
||||
if $LANG!= *"UTF-8"* || $LANG != *"utf-8"*; then
|
||||
if $LANG != *"UTF-8"* || $LANG != *"utf-8"*; then
|
||||
notice "Language environment variables are not set as expected."
|
||||
notice " You may need to set them to UTF-8."
|
||||
notice " Uncomment the LANG var in $VAR_FILE before sourcing to do so"
|
||||
echo "# uncomment the following lines to fix decoding errors e.g. hGetContents" >> $VAR_FILE
|
||||
echo "# uncomment the following line to fix decoding errors e.g. hGetContents" >> $VAR_FILE
|
||||
echo "# export LANG=C.UTF-8" >> $VAR_FILE
|
||||
fi;;
|
||||
*) return;;
|
||||
|
@ -7,8 +7,6 @@
|
||||
FROM ubuntu:20.04
|
||||
WORKDIR /home/
|
||||
|
||||
ENV LANG="C.UTF-8" LC_ALL="C.UTF-8"
|
||||
|
||||
RUN apt-get -y upgrade \
|
||||
&& apt-get -y update \
|
||||
&& apt-get install -y \
|
||||
@ -18,5 +16,8 @@ RUN ["git", "clone", "https://github.com/GaloisInc/cryptol.git"]
|
||||
|
||||
WORKDIR /home/cryptol
|
||||
RUN ["dev/dev_setup.sh"]
|
||||
RUN ["source", "dev/env.sh"]
|
||||
CMD ["/bin/sh"]
|
||||
|
||||
# Hardcode the environment variables we're going to need
|
||||
ENV LANG="C.UTF-8" LC_ALL="C.UTF-8" PATH=$PATH:/root/.ghcup/bin
|
||||
|
||||
CMD ["/bin/bash"]
|
||||
|
@ -7,8 +7,6 @@
|
||||
FROM ubuntu:22.04
|
||||
WORKDIR /home/
|
||||
|
||||
ENV LANG="C.UTF-8" LC_ALL="C.UTF-8"
|
||||
|
||||
RUN apt-get -y upgrade \
|
||||
&& apt-get -y update \
|
||||
&& apt-get install -y \
|
||||
@ -18,5 +16,8 @@ RUN ["git", "clone", "https://github.com/GaloisInc/cryptol.git"]
|
||||
|
||||
WORKDIR /home/cryptol
|
||||
RUN ["dev/dev_setup.sh"]
|
||||
RUN ["source", "dev/env.sh"]
|
||||
CMD ["/bin/sh"]
|
||||
|
||||
# Hardcode the environment variables we're going to need
|
||||
ENV LANG="C.UTF-8" LC_ALL="C.UTF-8" PATH=$PATH:/root/.ghcup/bin
|
||||
|
||||
CMD ["/bin/bash"]
|
||||
|
Loading…
Reference in New Issue
Block a user