Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[ci] pin user developments #13401

Merged
merged 1 commit into from Nov 18, 2020
Merged

[ci] pin user developments #13401

merged 1 commit into from Nov 18, 2020

Conversation

gares
Copy link
Member

@gares gares commented Nov 16, 2020

PR with overlays in 8.13+beta1 (not yet taken into account here are) are:
#12653
#13312
#13352
#13386

@gares gares added this to the 8.13+beta1 milestone Nov 16, 2020
@gares gares requested a review from Zimmi48 November 16, 2020 17:47
@gares gares requested a review from a team as a code owner November 16, 2020 17:47
@gares gares self-assigned this Nov 16, 2020
Zimmi48
Zimmi48 reviewed Nov 16, 2020
View reviewed changes
Copy link
Member

@Zimmi48 Zimmi48 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. CI will tell us if everything is fine.

@Zimmi48 Zimmi48 added the kind: infrastructure CI, build tools, development tools. label Nov 16, 2020
@gares
Copy link
Member Author

gares commented Nov 16, 2020 •
edited

equations is waiting for an overlay mattam82/Coq-Equations#316
math comp is bogus, re running

@gares gares mentioned this pull request Nov 17, 2020
Merged
@gares gares force-pushed the pin-overlays branch 2 times, most recently from 5c1258e to c82ba7f Compare November 18, 2020 08:18
@gares
Copy link
Member Author

gares commented Nov 18, 2020

@coqbot merge now

@coqbot-app
Copy link
Contributor

coqbot-app bot commented Nov 18, 2020

@gares: You can't merge the PR because you are the author.

@gares
Copy link
Member Author

gares commented Nov 18, 2020

ah ah, we will see @coqbot

@gares gares merged commit 7b2f311 into coq:v8.13 Nov 18, 2020
@coqbot-app coqbot-app bot added this to Shipped in 8.13+beta1 in Coq 8.13 Nov 18, 2020
@gares gares deleted the pin-overlays branch November 18, 2020 12:46
@Zimmi48
Copy link
Member

Zimmi48 commented Nov 18, 2020

Currently, coqbot can only merge in master. I haven't implemented the logic of merging into release branches because it is quite different from the one of the master branch (in principle, we would need the RM info, but we could just check that the author of the comment is in the @coq/core team). Let me know if this is something that you would like to get or if it's not very important.

@gares gares restored the pin-overlays branch November 27, 2020 13:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Zimmi48 Zimmi48 Zimmi48 left review comments

Assignees

@gares gares

Labels
kind: infrastructure CI, build tools, development tools.
Projects
No open projects
Coq 8.13
Shipped in 8.13+beta1
Milestone
8.13+beta1
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@gares @Zimmi48