On Fri, Jan 24, 2020 at 10:37 PM Jordan Johnson <j...@fellowhuman.com> wrote: > > On 24 Jan 2020, at 14:00, Robby Findler <ro...@cs.northwestern.edu> wrote: > > In the preferences dialog, in the General tab, the last checkbox is > > the one you want. > > The one for saving files upon switching tabs? >
That new options is added in the upcoming v7.6 release. > > But let me confirm: the reason it is painful to turn on the preference > > is that you have to choose a file? > > Well, I hadn’t ever turned on the preference before, so I didn’t know whether > it would necessitate choosing a file. But in answer to your question, no. See > below. > > > Would it work well for you if it > > only wanted to save files that already had filenames? > > AFAICT now that I’ve turned on that preference, this is the behavior it has. > It doesn’t prompt me to save an untitled file. And this is the behavior I > would want, if DrR is saving upon tab-switching. > > It feels weird to me to have DrR save files when I switch tabs; I’m somewhat > trained to use the “modified” state as a marker that I’m in the middle of > something, and “is everything saved?” is a part of my “am I done?” mental > checklist when I’m working on multiple unrelated things in different tabs. > I’ll have to impose a different discipline on myself (which may be for the > best). > > For now, I’ll try living with the preference enabled for a while. I don’t > foresee doing any complicated work this spring, so it’s no big deal right now. > > Thanks for the reply. > > Cheers, > Jordan > > -- > 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. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/2702DF36-1CB7-40F3-AF5D-3D0AABC8D395%40fellowhuman.com. -- 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. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAMTzy%2BYUdVmvwY7atim68BgRR5cCzDv_nHO%2BvwxxQ%2BiQSqpAFw%40mail.gmail.com.