equal
deleted
inserted
replaced
75 |
75 |
76 Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology |
76 Option \<^verbatim>\<open>-p\<close> includes additional Ubuntu packages, using the terminology |
77 of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution. |
77 of \<^verbatim>\<open>apt-get install\<close> within the underlying Linux distribution. |
78 |
78 |
79 Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as |
79 Option \<^verbatim>\<open>-P\<close> refers to high-level package collections: \<^verbatim>\<open>X11\<close> or \<^verbatim>\<open>latex\<close> as |
80 provided by \<^verbatim>\<open>isabelle build_docker\<close> (assuming Ubuntu 18.04 LTS). This |
80 provided by \<^verbatim>\<open>isabelle build_docker\<close> (assuming Ubuntu 20.04 LTS). This |
81 imposes extra weight on the resulting Docker images. Note that \<^verbatim>\<open>X11\<close> will |
81 imposes extra weight on the resulting Docker images. Note that \<^verbatim>\<open>X11\<close> will |
82 only provide remote X11 support according to the modest GUI quality |
82 only provide remote X11 support according to the modest GUI quality |
83 standards of the late 1990-ies. |
83 standards of the late 1990-ies. |
84 |
84 |
85 \<^medskip> |
85 \<^medskip> |