Repository navigation
Merge-queue: HOL-Light proofs do not gate merges #1281
Description
The merge queue merges a PR as soon as the required status checks have passed. This currently only includes the CI Summary and DCO, i.e., it excludes the HOL-Light proofs. I have observed a merge of #1269 before the corresponding HOL-Light proofs had passed.
Activity