[go: up one dir, main page]
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

Fix ppvernac on Goal: don't print an underscore for the missing name #17171

Merged
merged 1 commit into from
Feb 9, 2023
Merged

Fix ppvernac on Goal: don't print an underscore for the missing name #17171

merged 1 commit into from
Feb 9, 2023

Conversation

SkySkimmer
Copy link
Contributor

No description provided.

@SkySkimmer SkySkimmer requested a review from a team as a code owner January 26, 2023 10:26
@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 Jan 26, 2023
@Alizter Alizter added needs: test-suite update Test case should be added to / updated in the test-suite. and removed needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Jan 26, 2023
@Alizter
Copy link
Contributor
Alizter commented Jan 26, 2023

@coqbot run full ci

@Alizter Alizter added kind: infrastructure CI, build tools, development tools. part: vernac High level command interpretation. labels Jan 26, 2023
@Alizter Alizter added this to the 8.18+rc1 milestone Jan 26, 2023
@Alizter Alizter self-assigned this Jan 26, 2023
@SkySkimmer SkySkimmer removed the needs: test-suite update Test case should be added to / updated in the test-suite. label Jan 31, 2023
@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 Jan 31, 2023
@SkySkimmer
Copy link
Contributor Author

@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 Feb 7, 2023
@Alizter
Copy link
Contributor
Alizter commented Feb 7, 2023

@coqbot run full ci

@Alizter
Copy link
Contributor
Alizter commented Feb 9, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit e536726 into coq:master Feb 9, 2023
@SkySkimmer SkySkimmer deleted the ppgoal branch February 9, 2023 18:08
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Alizter Alizter Alizter approved these changes

Assignees

@Alizter Alizter

Labels
kind: infrastructure CI, build tools, development tools. part: vernac High level command interpretation.
Projects
None yet
Milestone
8.18+rc1
Development

Successfully merging this pull request may close these issues.
2 participants
@SkySkimmer @Alizter