Merge "Replace some javadoc symbols with HTML encoding" into rvc-dev