[isabelle-dev] NEWS: isabelle jedit options

[Makarius]

On 06/06/18 12:45, Lawrence Paulson wrote:
> I saw them of course, but what do they do?

These options go back to Nov-2017, but in recent Isabelle/bcdc47c9d4af I
have simplified and clarified the situation, updated NEWS and
documentation in the "jedit" manual.

Right now the main question is if this is sufficient for the release,
and the documentation clear.


	Makarius