DrRacket's font configuration is the first pane in the preferences dialog; you will probably find it at the bottom of the Edit menu, I guess?
If that wasn't where you were looking when you were talking about DrRacket's decision making earlier, can you elaborate please? Robby On Sun, Jun 25, 2017 at 1:37 PM, Lehi Toskin <lehi.tos...@gmail.com> wrote: > Where is "Other..."? I don't see it anywhere. Also, `(get-face-list 'mono)` > shows a whole lot more fonts than just Monospace. > > On Sunday, June 25, 2017 at 3:33:22 AM UTC-7, Robby Findler wrote: >> DrRacket uses the result of (get-face-list 'mono) in its dialog. If >> you choose "Other..." you should be able to choose from the same set >> that get-font-from-user uses. >> >> Robby >> > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to racket-users+unsubscr...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to racket-users+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
