Is it possible to push a tag?

[DanOpcode]

I created a tag with:

jj tag set -r @- v1.0.0

Is it possible to then push it with a jj command? Now I ended up pushing with git instead:

git push --tags

[yuja]

No. Something like jj git push --tag NAME isn't implemented yet.

[DanOpcode]

Understand. That's what I suspected. I read through the help page for jj git push and didn't see anything about it. Thanks anyways! git push --tags works as well.

[warrenbhw]

might take a stab at this, will update when I have a PR up

[yuja]

I think we'll first need to redesign jj git fetch in a way that remote tags are tracked separately from local tags. Currently, we don't know the remote state of tags, so we cannot safely push moved tags with force-with-lease mode.

#7528