proper latex setup;
authorwenzelm
Sat Mar 23 19:50:03 2019 +0100 (4 weeks ago)
changeset 6995870dc3c4e9469
parent 69957 e3217c6d6467
child 69959 795ca58cee29
proper latex setup;
src/Pure/Tools/build_docker.scala
     1.1 --- a/src/Pure/Tools/build_docker.scala	Sat Mar 23 17:10:53 2019 +0100
     1.2 +++ b/src/Pure/Tools/build_docker.scala	Sat Mar 23 19:50:03 2019 +0100
     1.3 @@ -19,7 +19,8 @@
     1.4  
     1.5    val package_collections: Map[String, List[String]] =
     1.6      Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),
     1.7 -      "latex" -> List("texlive-fonts-extra", "texlive-latex-extra", "texlive-math-extra"))
     1.8 +      "latex" ->
     1.9 +        List("texlive-fonts-extra", "texlive-font-utils", "texlive-latex-extra", "texlive-science"))
    1.10  
    1.11    def build_docker(progress: Progress,
    1.12      app_archive: String,
    1.13 @@ -46,6 +47,7 @@
    1.14  SHELL ["/bin/bash", "-c"]
    1.15  
    1.16  # packages
    1.17 +ENV DEBIAN_FRONTEND=noninteractive
    1.18  RUN apt-get -y update && \
    1.19    apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \
    1.20    apt-get clean