We don´t use the build script anymore

Author: vmcj

.github/workflows/build-gitlab-container-PR.yml

@@ -48,6 +48,17 @@ jobs:
         with:
           images: ghcr.io/${{ github.repository }}
 
+      - name: Building an example chroot...
+        run: |
+          wget https://github.com/DOMjudge/domjudge/archive/refs/heads/main.zip
+          unzip main.zip
+          cd domjudge-main
+            make configure
+            ./configure --with-domjudge-user=domjudge --with-judgehost_chrootdir="$(pwd)/chroot"
+          cd misc-tools
+            make dj_make_chroot
+            sudo ./dj_make_chroot
+
       - name: Build and push Docker images
         uses: docker/build-push-action@v5
         with:

docker-gitlabci/build.sh

@@ -1,5 +1,6 @@
 #!/bin/bash -e
 
+# This script is not used in GHA CI
 if [[ -n ${CI} ]]
 then
         set -euxo pipefail
@@ -20,16 +21,6 @@ else
 	REGISTRY=$2
 fi
 
-echo "[..] Building an example chroot..."
-wget https://github.com/DOMjudge/domjudge/archive/refs/heads/main.zip
-unzip main.zip
-cd domjudge-main
-  make configure
-  ./configure --with-domjudge-user=domjudge --with-judgehost_chrootdir="$(pwd)/chroot"
-cd misc-tools
-  make dj_make_chroot
-  sudo ./dj_make_chroot
-
 echo "[..] Building Docker image for Gitlab CI..."
 cp -r ../docker-contributor/php-config ./
 docker build -t "${REGISTRY}:${VERSION}" .