Re: [isabelle] Error messages in RC2014-RC4



On 29.08.2014 05:11, Alfio Martini wrote:
> Dear Makarius,
>
> Maybe it is a little too late for that, but I have just noticed that error
> messages in the RC4 version are showing a strange typographical
> symbol. I think there is something to be adjusted here. See image
> for an example. I am using the Windows version.
This is intended: Ctrl+clicking on this symbol takes you to the position
of the error.

  -- Lars




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