[Feature] mirroring to inria gitlab

Open
  • Is something wrong?
#16 6 comments 0 reactions 2 assignees View on GitHub

Maintainers usually reply within 1 day

@srcansiz is already working on this.

Since Mar 22, 2025.

Assessment

This issue has not been assessed yet.

Description

enhancement

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

Dominant language
Julia
Stars
1
Forks
0
Avg merge
1h 39m
Merged PRs (30d)
45

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from control-toolbox/CTActions

All issues in control-toolbox/CTActions

Similar issues

More Julia issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.