On Tuesday, April 9, 2024 at 4:20:56 PM UTC-7 Dima Pasechnik wrote: have a CI/sage-distro repo [...] with all that .github/ etc stuff needed for CI, including a part of build/ - and checkout sagelib as a submodule.
Also that does not work. Part of the .github/workflows is to run the CI on the pull requests for the Sage library, and the .devcontainer is for making GitHub Codespaces available on the pull requests for the Sage library. -- 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/604274c5-e7ac-41ef-a2b4-8bef436a91a8n%40googlegroups.com.
