From 2d53c7cfb8925fa11b2cb10d737215b5478bf6f7 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Tue, 11 Dec 2007 13:19:23 +0000 Subject: [PATCH] add --no-planet option to setup-plt svn: r7957 original commit: 487a71bf0d638f04602690bacef7e1762a447f32 --- collects/setup/option-sig.ss | 1 + 1 file changed, 1 insertion(+) diff --git a/collects/setup/option-sig.ss b/collects/setup/option-sig.ss index cd577e538e..89e69d5124 100644 --- 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