search

INCATools / ontology-development-kit

Bootstrap an OBO Library ontology
http://incatools.github.io/ontology-development-kit/
BSD 3-Clause "New" or "Revised" License
212 stars 53 forks source link

Update the documentation on ROBOT plugins. #1009

Closed gouttegd closed 4 months ago

gouttegd commented 4 months ago

This commit updates the page on the use of ROBOT plugins to: (1) add the KGCL plugin to the list of plugins that are bundled with the ODK (so that people know they don't need to manually configure that plugin), and (2) use the Uberon plugin rather than the KGCL plugin in examples about how to configure a non-bundled plugin, to avoid needless confusion.

(This should have been done as part of #995.)

gouttegd commented 4 months ago

Any idea on what’s going on with the CI check? It has been stuck on “waiting for status to be reported” ever since I created the PR, and I can’t merge anything until it’s done.

anitacaron commented 4 months ago

The conflict between not needing to run QC because it's just a change in an MD file and the need to pass QC to be able to merge?

gouttegd commented 4 months ago

The conflict between not needing to run QC because it's just a change in an MD file and the need to pass QC to be able to merge?

If so, that’s pretty dumb from GitHub. I would have expected that the workflow not running at all (because the PR doesn’t meet the criteria) would count as a pass. 🤦

gouttegd commented 4 months ago

If so, that’s pretty dumb from GitHub.

And yet that is exactly the case:

If a workflow is skipped due to path filtering, branch filtering or a commit message (see below), then checks associated with that workflow will remain in a "Pending" state. A pull request that requires those checks to be successful will be blocked from merging.

So basically a PR that only changes the documentation (and therefore won’t trigger the CI workflow) can’t be merged.

Am I supposed to push a commit with a dummy change in the “code” part of the repository just so that we can run a completely useless CI check just so that I can merge a documentation change? The level of stupidity is staggering.

gouttegd commented 4 months ago

Fuck it, the doc will remain not updated until I have some unrelated code changes to push. Not going to make a dummy commit just to make GitHub happy.

matentzn commented 4 months ago

Why didn't you just merge this?

gouttegd commented 4 months ago

Because I cannot! We require that the CI check must pass before merging is allowed, but the CI workflow doesn’t run on a PR that only changes the documentation. And GitHub, in its infinite wisdom, considers that a workflows that doesn’t run is a workflow that doesn’t pass.