At Tue, 11 Aug 2009 12:30:23 -0400, Carl Eastlund wrote: > On Tue, Aug 11, 2009 at 12:29 PM, Matthew Flatt<mfl...@cs.utah.edu> wrote: > > Do any of your linked planet packages refer to regular Planet packages > > (which must be downloaded and installed)? > > Yes.
Ah, that must be it. After the Planet package is installed, Planet attempts to update the user-specific documentation index. But the rest of the documentation files are not in shape for a mere "update". If you don't use -D, then `setup-plt' eventually starts working on documentation. It fixes the user-specific documentation index, so everything is right in the end --- but you see error messages along the way. I'm not immediately sure how to fix this, and I'll think about it more. _________________________________________________ For list-related administrative tasks: http://list.cs.brown.edu/mailman/listinfo/plt-dev
