The source code it probably here
https://sourceforge.net/p/jump-pilot/code/HEAD/tree/core/trunk/src/com/vividsolutions/jump/workbench/ui/plugin/BeanShellPlugIn.java
but I am not good enough att reading the code to tell where the font is either
set or perhaps leaved as default.
---
** [support-requests:#7] BeanShell Script Editor properties**
**Status:** open
**Labels:** beanshell beanshell script editor bsheditor4jump properties
**Created:** Wed Jun 10, 2020 08:08 AM UTC by kjt
**Last Updated:** Wed Jun 10, 2020 08:08 AM UTC
**Owner:** nobody
I would like to change the font type and/or font size in the BeanShell Script
Editor.
How can I do it...?
---
Sent from sourceforge.net because jump-pilot-devel@lists.sourceforge.net is
subscribed to https://sourceforge.net/p/jump-pilot/support-requests/
To unsubscribe from further messages, a project admin can change settings at
https://sourceforge.net/p/jump-pilot/admin/support-requests/options. Or, if
this is a mailing list, you can unsubscribe from the mailing list.
_______________________________________________
Jump-pilot-devel mailing list
Jump-pilot-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/jump-pilot-devel
