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 minimization] File name should include project info rather than be `bug.v` #292

Open

JasonGross opened this issue Sep 2, 2023 · 0 comments

Labels

Member

JasonGross commented Sep 2, 2023

Suggested by @herbelin , I believe, on the feedback survey

This plausibly needs some edits on the bug minimizer runner, and we'll need to edit the yml job to have the custom file name

JasonGross added the bug minimizer label

JasonGross added this to Coq Bug Minimizer

github-project-automation bot moved this to Todo in Coq Bug Minimizer

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment