Re: Increase Frequency of Updates of RTEMS GitHub Tools Mirroring

Hello Chris, Am 27.10.22 um 23:55 schrieb Chris Johns: Hi Christian, Thank you for your considered comments. On 27/10/2022 12:06 am, Christian MAUDERER wrote: Am 26.10.22 um 01:06 schrieb Chris Johns: On 26/10/2022 4:46 am, Joel Sherrill wrote: In general, our current approach is

Re: Increase Frequency of Updates of RTEMS GitHub Tools Mirroring

Hi Christian, Thank you for your considered comments. On 27/10/2022 12:06 am, Christian MAUDERER wrote: > Am 26.10.22 um 01:06 schrieb Chris Johns: >> On 26/10/2022 4:46 am, Joel Sherrill wrote: >>> In general, our current approach is quite a hack. We should do things >>> more event

Re: Increase Frequency of Updates of RTEMS GitHub Tools Mirroring

Am 26.10.22 um 01:06 schrieb Chris Johns: On 26/10/2022 4:46 am, Joel Sherrill wrote: In general, our current approach is quite a hack. We should do things more event driven. For example, if you want to update the RSB, then you create a pull request. This pull request starts a CI

Re: Increase Frequency of Updates of RTEMS GitHub Tools Mirroring

On 26/10/2022 4:46 am, Joel Sherrill wrote: > In general, our current approach is quite a hack. We should do things > more event driven. For example, if you want to update the RSB, then you > create a pull request. This pull request starts a CI script which > updates the mirrors

Re: Increase Frequency of Updates of RTEMS GitHub Tools Mirroring

On 25/10/2022 19:46, Joel Sherrill wrote: On Tue, Oct 25, 2022 at 2:41 AM Sebastian Huber > wrote: On 24/10/2022 21:27, Joel Sherrill wrote: > I'm not sure how often the GNU tools mirrors are updated for RTEMS > at GitHub but it would be

Re: Increase Frequency of Updates of RTEMS GitHub Tools Mirroring

On Tue, Oct 25, 2022 at 2:41 AM Sebastian Huber < sebastian.hu...@embedded-brains.de> wrote: > On 24/10/2022 21:27, Joel Sherrill wrote: > > I'm not sure how often the GNU tools mirrors are updated for RTEMS > > at GitHub but it would be appreciated if the frequency could be > increased. > > It

Re: Increase Frequency of Updates of RTEMS GitHub Tools Mirroring

On 24/10/2022 21:27, Joel Sherrill wrote: I'm not sure how often the GNU tools mirrors are updated for RTEMS at GitHub but it would be appreciated if the frequency could be increased. It seems to add a day to any tool update that requires using a git hash since the mirroring takes a while

Increase Frequency of Updates of RTEMS GitHub Tools Mirroring

Hi I'm not sure how often the GNU tools mirrors are updated for RTEMS at GitHub but it would be appreciated if the frequency could be increased. It seems to add a day to any tool update that requires using a git hash since the mirroring takes a while after the commit. I was updating the mips