Thanks Julian, I have seen that you also fixed some javadoc style (thought I had used <p> in all comments but apparently I missed a few).
-- Jesús On 4/26/17, 11:16 PM, "Julian Hyde" <[email protected]> wrote: >OK, fixed now. > >> On Apr 26, 2017, at 2:22 PM, Julian Hyde <[email protected]> wrote: >> >> Jesus' last commit had some javadoc errors ("mvn javadoc:javadoc >> javadoc:test-javadoc" under JDK 1.9). I am fixing them and will commit >> shortly. > >
