mirror of
https://gitflic.ru/project/openide/openide.git
synced 2025-12-14 18:05:27 +07:00
there are two kinds of release tags: build-number-based and marketing-version-based, no need to trigger GitHub workflows for both since they're put on the same commits (cherry picked from commit 658ed5026db9903ac6a1cc0522100c05fd55ff79) GitOrigin-RevId: e140db86302cb37364cbd74290a154708f655f59