deprecated symbol not marked

What could be the reason that deprecated symbols are not marked as usual in
#9920? The "Deprecated symbol" in the Java Colors & Fonts section has a
check box at Error Stripe Mark and Effects, but my file shows a green square
at the top right corner.

Thanks in advance,
Tom

Please sign in to leave a comment.