how to get special characters in hover tool

Sorry if this is a duplicate - couldn’t find an answer in the mailing list.

I’d like to put some special characters in a hover label, for example a less than sign. No matter how I try to encode it (\u003C, <), I can’t get it to show up.

For example:

Look at the data for hover_lab on line 238 in the javascript.