remove 'planet' from plt/bin (raco planet does the same thing and
planet conflicted with another package in Debian)
This commit is contained in:
parent
ec34fc6870
commit
258f267508
|
@ -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)))
|
||||
|
|
Loading…
Reference in New Issue
Block a user