Push --follow tags does not agree with its documentation

[Dennis Kaarsemaker <dennis@kaarsemaker.net>]

When deleting an annotated tag with git push -d while having
push.follwTags set to true, causes push to push other annotated tags. I
was surprised by this as this does not agree with the documentation

	Push all the refs that would be pushed without this option, and
	also push annotated tags in refs/tags that are missing from the
	remote but are pointing at commit-ish that are reachable from
	the refs being pushed. This can also be specified with
	configuration variable push.followTags. For more information,
	see push.followTags in git-config(1).

Note also that the tag pushed in error is not even reachable from the
tag that's being deleted.

$ git config push.followTags
true

$ git push origin --delete v2.5.1
To /tmp/whelk.git/
 - [deleted]         v2.5.1

$ git push origin --delete 2.5

Counting objects: 1, done.
Writing objects: 100% (1/1), 166 bytes | 0 bytes/s, done.
Total 1 (delta 0), reused 1 (delta 0)
To /tmp/whelk.git/
 - [deleted]         2.5
 * [new tag]         v2.5.1 -> v2.5.1

Which one is correct in this case, the behaviour or the documentation?
-- 
Dennis Kaarsemaker
www.kaarsemaker.net