Re: [isabelle] RC1: etc/symbols file from 2015 crashes jedit tool on startup



Am 21.01.16 um 14:18 schrieb Peter Lammich:
ERROR(Unknown
option "jedit_tooltip_delay")
Maybe this was renamed to jedit_completion_delay ? etc/preferences should be the file.

Best Benedikt




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.