I "made a release" in the sense of make all release followed by a merge into this repo's main. But I did not make a GitHub release. It doesn't look like that has ever been done before.
If BioPortal picks up the new release artifact(s) from this repo in the next day or two, then I will conclude that no further action is required.
I "made a release" in the sense of
make all releasefollowed by a merge into this repo's main. But I did not make a GitHub release. It doesn't look like that has ever been done before.If BioPortal picks up the new release artifact(s) from this repo in the next day or two, then I will conclude that no further action is required.