Skip to content

remove redundant options #9

remove redundant options

remove redundant options #9

# this jobs compares ./devcontainer/dodona-tested.dockerfile with the dockerfile in the repository dodona-edu/docker-images
# if they are different, a pull request is created in the dodona-edu/docker-images repository
name: Create pr for docker image
on:
pull_request:
types:
- closed
branches:
- master
jobs:
pr:
if: github.event.pull_request.merged == true
name: Create pr for docker image
runs-on: ubuntu-latest
steps:
- name: Checkout code
uses: actions/checkout@v4
- name: Send pull-request
env:
PR_NUMBER: ${{ github.event.number }}
REPOSITORY: dodona-edu/docker-images
TOKEN: ${{ secrets.PUSH_TO_DOCKER_IMAGES_ACCESS_TOKEN }}
USER: dodona-server
EMAIL: dodona@ugent.be
run: |
FOLDER="docker-images"
BRANCH_NAME="update-dodona-tested-$PR_NUMBER"
# Store the PAT in a file that can be accessed by the
# GitHub CLI.
echo "$TOKEN" > token.txt
# Authorize GitHub CLI for the current repository
gh auth login --with-token < token.txt
gh repo clone $REPOSITORY $FOLDER -- --depth=1
cd $FOLDER
# Setup the committers identity.
gh auth setup-git
# Setup the committers email and username, required until https://github.com/cli/cli/issues/6096 is resolved
git config --global user.name "$USER"
git config --global user.email "$EMAIL"
# Create a new feature branch for the changes.
git checkout -b $BRANCH_NAME
# Replace the dodona-tested.dockerfile with the one in the repository dodona-edu/universal-judge
# First, create a new file with the header to clarify that it is autogenerated
echo "# This file is autogenerated by the dodona-edu/universal-judge repository" > dodona-tested.dockerfile
echo "# Any changes will be overwritten by the CI" >> dodona-tested.dockerfile
echo "" >> dodona-tested.dockerfile
cat ../.devcontainer/dodona-tested.dockerfile >> dodona-tested.dockerfile
# check git status if the dockerfile has changed
# if not, exit
if [ -z "$(git status --porcelain)" ]; then
echo "No changes to the dockerfile"
exit 0
fi
# Commit the changes and push the feature branch to origin
git commit -am "Chore: update dodona-tested dockerfile"
git push origin $BRANCH_NAME
# Create a pull request in the remote repository
gh pr create \
--body "" \
--title "Update dodona-tested dockerfile to match pr #$PR_NUMBER" \
--body "This pr updates the dodona-tested dockerfile to match pr https://github.com/dodona-edu/universal-judge/pull/$PR_NUMBER" \
--head "$BRANCH_NAME" \
--base "master"