<html> <head> <meta content="text/html; charset=UTF-8" http-equiv="Content-Type"> </head> <body bgcolor="#FFFFFF" text="#000000"> I myself can no longer reproduce it after closing and reopening DrRacket. By coincidence, before closing it, the menus stopped working and I got a Ubuntu error of some sort as well. I shall keep trying for a bit.<br> <br> <div class="moz-cite-prefix">On 06/22/2013 03:12 PM, Robby Findler wrote:<br> </div> <blockquote cite="mid:CAL3TdOMcBSEeu2pgTxpvY+Bjqbuwyh-OpiHNTnmz7mXRdiqJBg@mail.gmail.com" type="cite"> <div dir="ltr">I'm not seeing that behavior (that is a bug, tho). I tried these steps: <div><br> </div> <div>1) cmd-t to create a new tab in DrRacket.</div> <div>2) paste the expression above (there is an automatic "#lang racket" inserted).</div> <div>3) save the file.</div> <div>4) delete the above expression</div> <div>5) hit run.<br> <div><br> </div> <div style="">No output observed.</div> <div style=""><br> </div> <div style="">Were you doing something differently?</div> <div><br> </div> <div style="">Robby</div> </div> </div> <div class="gmail_extra"><br> <br> <div class="gmail_quote">On Sat, Jun 22, 2013 at 2:02 PM, Sean Kanaley <span dir="ltr"><<a moz-do-not-send="true" href="mailto:skanaley@gmail.com" target="_blank">skanaley@gmail.com</a>></span> wrote:<br> <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I don't use modules very much, so this could be the defined behavior similar to how the ffi module "secretly" (it's actually documented) doesn't reload foreign libraries unless DrRacket is restarted, but I didn't notice anything in the documentation. How to reproduce:<br> <br> (module+ test<br> (write "?"))<br> <br> Without even running it, save the file, then delete that expression. Now run it (as in ctrl+r), and it will write "?".<br> ____________________<br> Racket Users list:<br> <a moz-do-not-send="true" href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br> </blockquote> </div> <br> </div> </blockquote> <br> </body> </html>