> Is this just needed for references from javadoc?  If so, then this can
> be copied to build/docs, no?

Yes. Committed.

Jérôme

Reply via email to