Closed bgamari closed 5 years ago
We do process milestone changes just like any other change; if other changes create notes, but milestones don't, then that's probably a gitlab issue.
If it is a gitlab "feature" (i.e., the issue isn't going to be fixed), we can of course fabricate "Trac metadata" comments ourselves.
This is now fixed.
See https://gitlab.home.smart-cactus.org/ghc/ghc/issues/16004. The last comment clearly describes a milestone change but there is no indication of what the milestone was before the change.