Hey,
Two days ago I created a tag for Diff [0]. While I'm writing this mail, the
tag has yet to appear on the GitHub mirror [1]. I made a commit after I
first noticed the tag did not appear to see if replicating that would also
sync the tags, which turned out not to be the case, as the commit made it
onto GitHub, while the tag did not show up.
We do not appear to have an appropriate component on bugzilla for this
piece of our infrastructure, so reporting the issue here.
[0] tag "0.8"
https://git.wikimedia.org/tags/mediawiki%2Fextensions%2FDiff.git
[1]
https://github.com/wikimedia/mediawiki-extensions-Diff/releases
Cheers
--
Jeroen De Dauw
http://www.bn2vs.com
Don't panic. Don't be evil. ~=[,,_,,]:3
--