Re: [racket-dev] rename "Help Desk" menu item

2011-06-30 Thread Robby Findler
Sounds like a good change to me. Robby On Fri, Jul 1, 2011 at 12:11 AM, Eli Barzilay wrote: > Four minutes ago, Neil Van Dyke wrote: >> Now that there is no longer a "Help Desk", can that menu item in >> DrRacket be renamed to something like "Documentation" or "Racket >> Documentation"? >> >> I

Re: [racket-dev] make-vector: out of memory making vector of length 0

2011-06-30 Thread Matthew Flatt
Sorry -- I thought I had pushed that fix along with the previous one. It's there now. At Thu, 30 Jun 2011 10:46:22 -0600, Jon Rafkind wrote: > I just updated to HEAD and I see this error during 'make install'. > > raco setup: making: compiler > raco setup: making: raco > make-vector: out of memor

[racket-dev] make-vector: out of memory making vector of length 0

2011-06-30 Thread Jon Rafkind
I just updated to HEAD and I see this error during 'make install'. raco setup: making: compiler raco setup: making: raco make-vector: out of memory making vector of length 0 make-vector: out of memory making vector of length 0 _ For list-related ad

Re: [racket-dev] rename "Help Desk" menu item

2011-06-30 Thread Eli Barzilay
Four minutes ago, Neil Van Dyke wrote: > Now that there is no longer a "Help Desk", can that menu item in > DrRacket be renamed to something like "Documentation" or "Racket > Documentation"? > > I think lots of users are reluctant enough to go to "Help" menus, > since they (Help menus, not users

[racket-dev] rename "Help Desk" menu item

2011-06-30 Thread Neil Van Dyke
Now that there is no longer a "Help Desk", can that menu item in DrRacket be renamed to something like "Documentation" or "Racket Documentation"? I think lots of users are reluctant enough to go to "Help" menus, since they (Help menus, not users) are usually full of useless filler crap. If a