ci: run tickgit after merging a PR in the devel branch#4241
Merged
mergify[bot] merged 1 commit intoceph:develfrom nixpanic:ci/tickgitNov 8, 2023
+23
tickgit after merging a PR in the devel branch#4241