Skip to content

Conversation

@SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented May 6, 2025

@SkySkimmer SkySkimmer added kind: internal API, ML documentation... request: full CI Use this label when you want your next push to trigger a full CI. labels May 6, 2025
@SkySkimmer SkySkimmer requested a review from a team as a code owner May 6, 2025 11:30
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 6, 2025
@SkySkimmer SkySkimmer added this to the 9.1+rc1 milestone May 6, 2025
@SkySkimmer SkySkimmer added the needs: overlay This is breaking external developments we track in CI. label May 6, 2025
SkySkimmer added a commit to SkySkimmer/MetaRocq that referenced this pull request May 6, 2025
SkySkimmer added a commit to SkySkimmer/coq-elpi that referenced this pull request May 6, 2025
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: overlay This is breaking external developments we track in CI. labels May 6, 2025
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label May 6, 2025
@ppedrot ppedrot self-assigned this May 7, 2025
ppedrot added a commit to MetaRocq/metarocq that referenced this pull request May 8, 2025
ppedrot added a commit to LPCIC/coq-elpi that referenced this pull request May 8, 2025
@ppedrot
Copy link
Member

ppedrot commented May 8, 2025

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 1477fcb into rocq-prover:master May 8, 2025
5 checks passed
@coqbot-app
Copy link
Contributor

coqbot-app bot commented May 8, 2025

@ppedrot: Please take care of the following overlays:

  • 20603-SkySkimmer-rm-depr-lib-apis.sh

@SkySkimmer SkySkimmer deleted the rm-depr-lib-apis branch May 9, 2025 11:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

kind: internal API, ML documentation...

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants