Skip to content

Commit d86f384

Browse files
committed
Remove old Dockerfile in root, unused afaict
1 parent 1f5a96c commit d86f384

File tree

2 files changed

+2
-32
lines changed

2 files changed

+2
-32
lines changed

Dockerfile

Lines changed: 0 additions & 31 deletions
This file was deleted.

admin/update_docker.sh

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,7 @@ if [ "${UPDATE_LATEST}" = "true" ]; then
7777
echo "Build complete. If you are happy with the images, run the following:"
7878
for IMAGE in minimal icpc full githubci; do
7979
echo " docker tag problemtools/${IMAGE}:${TAG} problemtools/${IMAGE}:latest"
80-
echo " docker push problemtools/${IMAGE}:${TAG} --all-tags"
80+
echo " docker push problemtools/${IMAGE}:${TAG}"
81+
echo " docker push problemtools/${IMAGE}:latest"
8182
done
8283
fi

0 commit comments

Comments
 (0)