From 258f267508a9676c4fbaca60b4db82caf1a36a94 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sat, 18 Aug 2012 20:26:50 -0500 Subject: [PATCH] remove 'planet' from plt/bin (raco planet does the same thing and planet conflicted with another package in Debian) --- collects/planet/info.rkt | 2 -- 1 file changed, 2 deletions(-) diff --git a/collects/planet/info.rkt b/collects/planet/info.rkt index 1866cf8ade..18212a717f 100644 --- a/collects/planet/info.rkt +++ b/collects/planet/info.rkt @@ -1,8 +1,6 @@ #lang setup/infotab (define name "PLaneT") -(define mzscheme-launcher-names '("planet")) -(define mzscheme-launcher-libraries '("planet.rkt")) (define scribblings '(("planet.scrbl" (multi-page) (tool)))) (define raco-commands '(("planet" planet/raco "manage Planet package installations" 80)))