@j-l-s @srcansiz hi, it would be nice (and safe) to set up a gitlab mirror of our current devs on github:
- by this I mean mirroring from github towards Inria gitlab
- this is know as a pull mirror on gitlab side
- the mirror is intended just for backup, no need to have a full / two way sync
- mirroring the main branch only is fine (no other branches, no issues / discussion, no wikis...)
The official gitlab doc is here but, when I take a look at what they say, I typically only see the push option for mirrors, not the pull. This can also be set up with github CI, as explained here.
Last but not least: IIRC, @nniclausse had a look at that. (possible issue: he might have written the action in erlang 🫢) Nicolas ?
@j-l-s @srcansiz hi, it would be nice (and safe) to set up a gitlab mirror of our current devs on github:
The official gitlab doc is here but, when I take a look at what they say, I typically only see the
pushoption for mirrors, not thepull. This can also be set up with github CI, as explained here.Last but not least: IIRC, @nniclausse had a look at that. (possible issue: he might have written the action in erlang 🫢) Nicolas ?