I'm pretty sure source files should be ISO-8859-1.
If you're more comfortable with entity tags appearing in a /* */ style
comment, then maybe that's what we should use for the header text.
(The Java Coding Guidlines say you should use a /* */ comment at the top
of the file.)