JMC-6180: Changing the Java source editor font changes the size of some values in the JMC tables
neugens at redhat.com
Tue Nov 20 17:12:49 UTC 2018
On Tue, 2018-11-06 at 15:06 +0100, Marcus Hirt wrote:
> Hi Elliott,
> Yes, I _think_ that would be the expected behavior from a user's
> If anyone thinks differently, please let me know and we can discuss
> the pros
> and cons.
I'm a bit concerned by the scope of this, do you think it would make
more sense to approach the patch incrementally?
>From what I gather this is quite a massive patch I'm not sure we want
that in before release.
> Kind regards,
> On 2018-11-05, 23:37, "jmc-dev on behalf of Elliott Baron" <
> jmc-dev-bounces at openjdk.java.net on behalf of ebaron at redhat.com>
> I'm working on a solution to this bug that allows the user to
> scale the
> font size used by JMC labels using the same shortcuts as
> Eclipse's text
> editor zoom-in/out functionality (which also simply scale the
> font size).
> Just to be clear, this functionality should scale font sizes for
> all JMC
> editors and views, and not just those using the Eclipse editor
Associate Manager, Software Engineering
Red Hat GmbH <https://www.redhat.com>
9704 A60C B4BE A8B8 0F30 9205 5D7E 4952 3F65 7898
More information about the jmc-dev