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

add deprecation warnings for Int31 #17734

Merged
merged 1 commit into from Jun 17, 2023
Merged

add deprecation warnings for Int31 #17734

merged 1 commit into from Jun 17, 2023

Conversation

andres-erbsen
Copy link
Contributor

No description provided.

@andres-erbsen andres-erbsen added kind: cleanup Code removal, deprecation, refactorings, etc. part: standard library The standard library stdlib. request: full CI Use this label when you want your next push to trigger a full CI. labels Jun 13, 2023
@andres-erbsen andres-erbsen added this to the 8.18+rc1 milestone Jun 13, 2023
@andres-erbsen andres-erbsen requested a review from a team as a code owner June 13, 2023 21:07
@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 Jun 13, 2023
@andres-erbsen andres-erbsen mentioned this pull request Jun 13, 2023
Closed
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 14, 2023

🔴 CI failure at commit 13cf58f without any failure in the test-suite

✔️ Corresponding job for the base commit ca8db7b succeeded

❔ Ask me to try to extract a minimal test case that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following target: ci-geocoq
  • You can also pass me a specific list of targets to minimize as arguments.

⚠️ ⌛ You may want to wait until the pipeline for the base commit (ca8db7b) finishes.

@proux01
Copy link
Contributor

proux01 commented Jun 14, 2023

Nice! The deprecated attributes should have a note statement telling to use the corresponding int63 module instead.

@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 14, 2023
proux01
proux01 approved these changes Jun 15, 2023
View reviewed changes
Copy link
Contributor

@proux01 proux01 left a comment

Choose a reason for hiding this comment

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

LGTM, will merge once CI is green

@proux01 proux01 self-assigned this Jun 15, 2023
@proux01
Copy link
Contributor

proux01 commented Jun 17, 2023

@coqbot run full ci

@coqbot-app coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Jun 17, 2023
@proux01
Copy link
Contributor

proux01 commented Jun 17, 2023

CI failures seem unrelated (same errors in other PRs) so let's merge.

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 2f40738 into coq:master Jun 17, 2023
5 of 8 checks passed
@olaure01 olaure01 mentioned this pull request Aug 24, 2023
Merged
2 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@proux01 proux01 proux01 approved these changes

Assignees

@proux01 proux01

Labels
kind: cleanup Code removal, deprecation, refactorings, etc. part: standard library The standard library stdlib.
Projects
None yet
Milestone
8.18+rc1
Development

Successfully merging this pull request may close these issues.

None yet
2 participants
@andres-erbsen @proux01