diff --git a/system/oio.sh b/system/oio.sh index 7480d5a..3c0f69c 100755 --- a/system/oio.sh +++ b/system/oio.sh @@ -205,7 +205,13 @@ case $1 in IpulldevI) + olddev=$(docker images -q ghcr.io/interlisp/online-medley:development) docker pull ghcr.io/interlisp/online-medley:development + newdev=$(docker images -q ghcr.io/interlisp/online-medley:development) + if [ -n "${olddev}" ] && [ "${olddev}" != "${newdev}" ] + then + docker image rm ${olddev} + fi echo "Online-medley development release pulled from Github Container Registry" ;;