2023-07-06 03:36:02 +12:00
|
|
|
FROM alnoda/alnoda-workspace:1.1
|
2022-09-09 09:40:57 +12:00
|
|
|
|
2023-07-06 03:36:02 +12:00
|
|
|
# Install Theia
|
|
|
|
|
RUN wrk install theia==1.29.0
|
|
|
|
|
|
|
|
|
|
# Copy custom Theia settings
|
2022-09-09 09:40:57 +12:00
|
|
|
COPY --chown=abc:abc theia_settings.json /home/abc/.theia/settings.json
|
2022-07-17 05:53:38 +12:00
|
|
|
|
2023-07-06 03:36:02 +12:00
|
|
|
# Set additional env vars
|
|
|
|
|
ENV SHELL=/bin/zsh USE_LOCAL_GIT=true
|
|
|
|
|
|
|
|
|
|
# Update Alnoda workspace UI, icons, fonts
|
2022-09-09 09:40:57 +12:00
|
|
|
COPY --chown=abc:abc workspace /tmp/workspace
|
2023-07-06 03:36:02 +12:00
|
|
|
RUN wrk build /tmp/workspace && rm -rf /tmp/workspace
|
