I will not respond further on this in this thread. On Thursday, April 11, 2024 at 1:15:52 PM UTC-7 Dima Pasechnik wrote:
> > > On 11 April 2024 21:47:57 CEST, Matthias Koeppe <matthia...@gmail.com> > wrote: > >Once again, the workflow files in .github/workflows have to be statically > >present in a repository so that Actions work. > >And the .devcontainers files have to be statically present in a > repository > >so that Codespaces work. > > Yes, sure, as I said, you can have it statically present, and test a > submodule containing sagelib from there. > > There is nothing hard to design here, once you split the repo this way. > > > > > >If you want to propose a design for breaking our repository into multiple > >repositories, work it out first. Learn about the relevant technological > >restrictions. > >It does not make sense to develop it here in a question-and-answer game. > >In particular, this cannot be done here in this thread about governance; > >it's only a distraction. > > > >Matthias > > > > > >On Thursday, April 11, 2024 at 12:36:20 PM UTC-7 Dima Pasechnik wrote: > > > >On 11 April 2024 18:06:42 CEST, Matthias Koeppe <matthia...@gmail.com> > >wrote: > >>On Thursday, April 11, 2024 at 4:28:12 AM UTC-7 dim...@gmail.com wrote: > >> > >>On Wed, Apr 10, 2024 at 04:23:13PM -0700, Matthias Koeppe wrote: > >>> On Wednesday, April 10, 2024 at 3:25:16 PM UTC-7 Dima Pasechnik wrote: > >>> Necessary reminder that we're discussing, as the subject says, the > files > >>> that control the GitHub workflows and the Codespaces. > >>> What a developer may do on their local machine does not matter. > >> > >>But there is no difference here between a CI and a local machine here. > >>A CI is perfectly capable of doing > >>"git submodule update --remote" > >>and proceed. > >> > >> > >>No. These files are processed by GitHub before any custom code can be > run. > > > >Are you saying that "git submodule..." cannot be triggered by > >repository_dispatch hook? > >So GH Actions cannot be triggered by a submodule update? > > > > > > > >> > > > -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/sage-devel/e49e8408-c44b-4179-8867-3c13e7a79e82n%40googlegroups.com.
