repo Option Doesn't Allow Changing Module Path
There is an ongoing gitlab.freedesktop.org outage that has prevented me from running any builds with JHBuild over the last couple of days: https://gitlab.freedesktop.org/freedesktop/freedesktop/-/issues/407
I thought that the repo
option might allow reconfiguring the repositories to use an alternative like the https://github.com/freedesktop mirror. However, the module path is different between the two. For example, for cairo:
cairo/cairo.git vs. freedesktop/cairo.git
So it doesn't appear that the repo option, as it currently exists, allows for doing this remapping.
Assuming we name the repo and module path something like: repo/module_path.parent/module_path.name
It would be nice if the repo option allowed setting both the repo and the module_path.parent: repos['gitlab.freedesktop.org']/module_path.parent = 'github.com/freedesktop' which would allow us to map the module path "name", like cairo.git, to the repo/module_path.parent