tree a02d165e1b5cbbfe35ae78404e2c813c54274094
parent e0e40d01d9d504d1639bb3f67082232247967dcb
author Luca Milanesio <luca.milanesio@gmail.com> 1614811215 +0100
committer Luca Milanesio <luca.milanesio@gmail.com> 1614811215 +0100

Allow publishing to different Docker registries

Recently, Dockerhub has become very slow and unstable
due to the introduction of hard limits on pulls and
throttling.

Make the prefix for all our CI images a configurable
variable, so that it becomes easy to switch to a
different Docker registry.

Change-Id: Ida613bfd1c3d9c779d2f522431ec8f4098c7bcfa