Increase Frequency of Updates of RTEMS GitHub Tools Mirroring

[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 script which
>     updates the mirrors and builds the RSB on a selected set of platforms.
>     If everything is all right, the pull request can be merged.
> 
> Just getting to the point where a pull request triggered an update would
> be useful. Assuming a pull request with no content would be ok.

I feel starting to have pull requests will only result in changes being posted
there by users who see pull requests as active. It is reasonable for a user to
think this. Who will then field those and merge them?

Chris