+1
Fortunately, nowadays the list of manuals shown in jEdit is very helpful
here.
Am Mittwoch, den 26.03.2014, 22:07 +0100 schrieb Florian Haftmann:
> Hi,
>
> since ancient times there is a glitch in the naming of manuals vs. their
> originating sessions, e.g. isar-ref vs. IsarRef.
>
> Would it
Hi,
since ancient times there is a glitch in the naming of manuals vs. their
originating sessions, e.g. isar-ref vs. IsarRef.
Would it be worth an effort to consolidate this? I regularly get
confused about that.
Cheers,
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/
