On 10 April 2024 02:04:48 CEST, Matthias Koeppe <matthiaskoe...@gmail.com>
wrote:
>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.
Regarding CI, triggering a git update+CI run on an event in another repo is
done via a repository_dispatch hook.
<https://docs.github.com/en/actions/using-workflows/events-that-trigger-workflows#repository_dispatch>
Indeed, it would be silly if one needed to pollute another repo with your CI
workflow files.
Dima
>
--
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/B44D0BAB-7B85-4121-B34E-5851FE72880E%40gmail.com.
