I guess that you probably have (had?) a default version of the preferences that has an old, less helpful regexp in it. You might not see any changes now, but you could also delete that line from the preferences file (and closing drr) and then open it again to get a good setting.
Sorry we changed that in a way that your (and other's) drr don't pick it up. Robby On Thu, Oct 12, 2017 at 6:04 AM Geoffrey Knauth <ge...@knauth.org> wrote: > Philip, thanks, that did it! I'll make a note of this in my hints file, > in case I have to do this again. > > Geoff > > -- > 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.
