> One final question: Is there a way to make the dot bold or bigger?
Since bold is already available (and you've set it) you'd probably need
to use a different character. I've not tracked down where that's
defined, nor even whether it's in a configuration file or in the source.
One of the developers could probably answer.
I guess it's theoretically possible a different text font might (?) have
a bolder appearing character for space, but that would take
experimentation.
Len
_______________________________________________
Users mailing list -- users@lists.geany.org
To unsubscribe send an email to users-le...@lists.geany.org
