Updating GitHub Mirrors?

[oss at c-mauderer.de]

Hello Joel and Sebastian,

Am 04.07.24 um 19:38 schrieb Sebastian Huber:
> ----- Am 4. Jul 2024 um 19:30 schrieb Joel Sherrill joel at rtems.org:
> 
>> Thanks. What times?
> 
> About 7 minutes past 4, 12, and 20 CEST.
> 

I'm not entirely sure how the mirroring is currently set upm, but it 
sounds like a cron job. Shouldn't our new gitlab support that out of the 
box:

https://docs.gitlab.com/ee/user/project/repository/mirror/push.html

Best regards

Christian