Build the shell configuration into the resources

The shell configuration was copied from the server by hand. It now has
its own directory, which make_files.py copies into the resources, so
that the resources are the whole set of files the cleanup restores and
nothing has to be copied by hand.

Co-Authored-By: Claude Code <noreply@anthropic.com>
This commit is contained in:
Zebreus 2026-10-25 13:05:22 +01:00
commit 917e3d6089

View file

@ -1,7 +1,9 @@
# Builds README, README.en, CODE_OF_CONDUCT and CODE_OF_CONDUCT.en in ../resources: the website's pages as
# terminal text with escape sequences, for the home directory of the shell server's root user.
# Builds the files for the home directory of the shell server's root user in ../resources: README, README.en,
# CODE_OF_CONDUCT and CODE_OF_CONDUCT.en as the website's pages in terminal text with escape sequences, and the
# shell configuration from ../shell.
# Usage: python3 server/scripts/make_files.py
import pathlib
import shutil
import textwrap
ESC = '\x1b'
@ -334,3 +336,6 @@ out.mkdir(exist_ok=True)
for name, text in [('README', readme(DE)), ('README.en', readme(EN)),
('CODE_OF_CONDUCT', code_of_conduct(COC_DE)), ('CODE_OF_CONDUCT.en', code_of_conduct(COC_EN))]:
(out / name).write_text(text, encoding='utf-8')
# The shell configuration is not generated, it is copied from ../shell, where it is edited.
for name in '.zshrc', '.zshenv':
shutil.copyfile(pathlib.Path(__file__).parent.parent / 'shell' / name, out / name)