On Friday 20 May 2016 07:48:09 Tom Browder wrote: > > or edit padre's preference to use another font. > > But I don't see how to do that--help, please.
You may be able to change fonts with Padre's preferences (or settings). Unfortunately, I cannot check on my system: padre no longer runs on Debian/unstable. Hope this helps -- https://github.com/dod38fr/ -o- http://search.cpan.org/~ddumont/ http://ddumont.wordpress.com/ -o- irc: dod at irc.debian.org _______________________________________________ Padre-dev mailing list Padre-dev@perlide.org http://mail.perlide.org/mailman/listinfo/padre-dev
