That woulds like a good change.
Meanwhile, whatever problem I was having pushing to github seems to have vanished now.
cheers M
On Wed, Oct 26, 2022 at 05:05:55PM +0200, IOhannes m zmölnig wrote:
Hi all (but sorry, miller really) -
On 10/24/22 17:46, IOhannes m zmölnig wrote:
maybe things have changed a bit since i originally setup the mirroring and they could be simplified.
so i've re-evaluated the options for synching, and it seems i have found a solution that is now somewhat faster (whenever you push something to github, our CI is now notified directly¹ that it should sync again).
i also tried to push some tags directly to the 'master' branch on github, and they immediately showed up. either the issue miller was having has been resolved magically on the github side, or it is really something odd going on with miller's pushes. if the problem still persists, there's also the option to create a tag directly via the webinterface which you (miller) could use instead of the temporary branch dance.
gmdsar IOhannes
¹ well "more directly" at least. our git-server recieves a notification that it should sync, then a CI job is run that syncs the repositories which in turn triggers another CI run that re-builds whatever needs rebuilding)
Pd-dev mailing list Pd-dev@lists.iem.at https://lists.puredata.info/listinfo/pd-dev