docker: fix publish workflow
Created by: LawnGnome
Since a credential rotation, the GitHub Action responsible for pushing the src-batch-change-volume-workspace has been failing. This action works as expected when used via Docker outside of the GitHub Action infrastructure; I suspect there's an issue with the handling of a particular character in the action-specific entry script.
That said, there's not much reason to pull in a third party action here; the push script already has the required credentials, and the Docker Hub API, while undocumented, is straightforward. I've added the required urllib-foo to make this happen. (I'd normally pull in Python's excellent requests library for this kind of thing, but that means we'd have to start installing dependencies in the GitHub Action that runs this script, and that feels like more effort than I'm really willing to go to here.)
Fixes #548.