Skip to content

bot no longer handles CI minimize comments #367

@JasonGross

Description

@JasonGross

I see

Unhandled comment: @coqbot minimize
```bash
#!/usr/bin/env bash
opam install -y coq-fiat-crypto
```

And

Unhandled comment: Checking if a shorter script works: 
@coqbot minimize coq.dev
```bash
#!/usr/bin/env bash
opam install -y coq-fiat-crypto
```

At https://github.com/organizations/rocq-prover/settings/apps/coqbot-app/advanced

Presumably something has gone wrong in regex parsing. This worked when rocq-prover/rocq#21513 (comment) was submitted but not shortly after at rocq-prover/rocq#21513 (comment) (about 2 weeks ago)

Metadata

Metadata

Labels

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions