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. -- 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/7c04399f-9b63-4bb1-a7ca-4ac0687dc776n%40googlegroups.com.
