Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

The teammanual is already installed in the image #178

Closed
wants to merge 6 commits into from
Closed

The teammanual is already installed in the image #178

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
b54f82e
The teammanual is already installed in the image
vmcj Mar 21, 2024
5431a3b
Since we have mergequeues this can be simpler
vmcj Mar 21, 2024
5432824
Remove (but trigger the CI for now..)
vmcj Mar 21, 2024
d0bb22b
Only run in our own space
vmcj Mar 21, 2024
6d9f918
No idea why I put this here
vmcj Mar 21, 2024
043b126
Remove
vmcj Mar 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
16 changes: 6 additions & 10 deletions .github/workflows/build-domjudge-container-PR.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,11 +11,6 @@ env:

jobs:
pr-domjudge:
if: ${{ !(github.repository == 'domjudge/domjudge-packaging' &&
github.ref == 'refs/heads/main') &&
!contains(github.ref, 'gh-readonly-queue') &&
(github.event_name == 'pull_request_target' ||
github.event.pull_request.head.repo.full_name != github.repository) }}
runs-on: ubuntu-latest
steps:
- name: Checkout
Expand Down Expand Up @@ -58,18 +53,19 @@ jobs:
run: |
cd docker
set -x
sh ./build.sh "${{ env.DOMJUDGE_VERSION }}" ${{ github.actor }}
sh ./build.sh "${{ env.DOMJUDGE_VERSION }}" domjudge
set +x

- run: docker image list

- name: Build and push
run: |
for IMG in domserver judgehost default-judgehost-chroot; do
IMAGE_NAME="${GITHUB_REPOSITORY_OWNER@L}/$IMG:${{ env.DOMJUDGE_VERSION }}"
docker image tag "$IMAGE_NAME" ghcr.io/${GITHUB_REPOSITORY_OWNER@L}/$IMG:${{ env.PR_TAG }}
docker image tag "$IMAGE_NAME" ${GITHUB_REPOSITORY_OWNER@L}/$IMG:${{ env.PR_TAG }}
docker push ghcr.io/${GITHUB_REPOSITORY_OWNER@L}/$IMG:${{ env.PR_TAG }}
IMAGE_NAME="domjudge/$IMG:${{ env.DOMJUDGE_VERSION }}"
echo "$IMAGE_NAME"
docker image tag "$IMAGE_NAME" ghcr.io/domjudge/$IMG:${{ env.PR_TAG }}
#docker image tag "$IMAGE_NAME" domjudge/$IMG:${{ env.PR_TAG }}
docker push ghcr.io/domjudge/$IMG:${{ env.PR_TAG }}
done

- name: Check for wrong permisions
Expand Down
2 changes: 0 additions & 2 deletions docker/domserver/Dockerfile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,6 @@ RUN apt update \
php-gmp php-xml php-mbstring \
sudo bsdmainutils ntp libcgroup-dev procps \
python3-venv fontconfig \
texlive-latex-recommended texlive-latex-extra \
texlive-fonts-recommended texlive-lang-european latexmk tex-gyre \
libcurl4-gnutls-dev libjsoncpp-dev libmagic-dev \
enscript lpr ca-certificates \
&& rm -rf /var/lib/apt/lists/*
Expand Down
Loading