Skip to content

Do not "add OBO shorthands" to the RO mirror.#3359

Merged
gouttegd merged 2 commits intomasterfrom 3016-dont-add-obo-shorthands-to-ro-mirrorOct 8, 2024

Commits