-
Georges Racinet authored
This is supposed to be equivalent to ci/release_docker_images, hence able to produce and push multi-platforms images, with the difference that it is currently only for the main image and much more maintainable. Perhaps we'll want to make a single script being able to handle also the case of the helper image, but in that case it will have clear options to make one, the other or both to avoid painful delays on low bandwidth connections because just one failed.