Convert these extracomment to comment
Because:
- We have a bug in our scripts that makes extracomment not work (will try to fix this asap)
- Makes sense to be a comment since we want it to be a disambiguation text
- KUIT markers (e.g. @label) need to be in comment