Skip to content

[Feature] mirroring to inria gitlab #16

@jbcaillau

Description

@jbcaillau

@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 ?

Metadata

Metadata

Assignees

Labels

enhancementNew feature or request

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions