add --no-planet option to setup-plt

svn: r7957 original commit: 487a71bf0d
2007-12-11 13:19:23 +00:00 · 2007-12-11 13:19:23 +00:00 · 2d53c7cfb8
commit 2d53c7cfb8
parent 553733c465
1 changed files with 1 additions and 0 deletions
--- a/collects/setup/option-sig.ss
+++ b/collects/setup/option-sig.ss
@ -15,6 +15,7 @@
     make-info-domain
     make-launchers
     make-docs
+     make-planet
     call-install
     call-post-install
     pause-on-errors