<div dir="ltr">Looks great to me. Sorry for not checking first.<div><br></div><div>Thanks,</div><div>Robby</div></div><div class="gmail_extra"><br><br><div class="gmail_quote">On Thu, May 30, 2013 at 6:51 AM, Matthew Flatt <span dir="ltr"><<a href="mailto:mflatt@cs.utah.edu" target="_blank">mflatt@cs.utah.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">At Wed, 29 May 2013 21:45:23 -0500, Robby Findler wrote:<br>
> re: current-directory-for-user: I also don't see a better way. Probably the<br>
> docs should say "don't set this path", roughly (with some caveats that<br>
> would include things like drracket)<br>
<br>
</div>Do the current docs say that well enough, or should we revise?:<br>
<br>
Normally, current-directory-for-user should stay at its initial value,<br>
reflecting the directory where a user started a process. A tool such<br>
as DrRacket, however, implicitly lets a user select a directory (for<br>
the file being edited), in which case updating<br>
current-directory-for-user makes sense.<br>
<br>
</blockquote></div><br></div>