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: > > On Wed, Apr 10, 2024 at 11:10 PM Matthias Koeppe <matthia...@gmail.com> > wrote: > > On Wednesday, April 10, 2024 at 2:40:18 PM UTC-7 Dima Pasechnik wrote: > > There is simply no need to keep the .gitsubmodules - > > the only file in the main repo affected by "git submodule update --remote" > - > always synchronized, commit-wise, for everyone. > > > There is. Without doing that, the changes made in the submodule won't take > effect. > > This is not true. > > git submodule update --remote > > will pick up submodules changes just fine. > > > 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. > > -- > 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/b178151b-6c80-4a8c-a93d-04fc824f969dn%40googlegroups.com. -- 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/Zhe2Ke9VxXXQFFco%40hilbert.homenet.telecomitalia.it.
signature.asc
Description: PGP signature
