From 511343114fe59b1f9caf2477d0d1bb0b55cef076 Mon Sep 17 00:00:00 2001 From: Jay McCarthy Date: Tue, 8 Jan 2008 18:27:59 +0000 Subject: [PATCH] Removing MrEd launcher, renaming some things svn: r8261 --- collects/web-server/info.ss | 9 ++------- collects/web-server/private/{launch-gui.ss => gui.ss} | 0 collects/web-server/private/{launch-text.ss => main.ss} | 0 3 files changed, 2 insertions(+), 7 deletions(-) rename collects/web-server/private/{launch-gui.ss => gui.ss} (100%) rename collects/web-server/private/{launch-text.ss => main.ss} (100%) diff --git a/collects/web-server/info.ss b/collects/web-server/info.ss index 47e9e20d28..24b0769d7e 100644 --- a/collects/web-server/info.ss +++ b/collects/web-server/info.ss @@ -4,11 +4,6 @@ ("docs/guide/web-guide.scrbl" (multi-page main-doc)))) (define mzscheme-launcher-libraries - (list "private/launch-text.ss")) + (list "private/main.ss")) (define mzscheme-launcher-names - (list "PLT Web Server Text")) - - (define mred-launcher-libraries - (list "private/launch-gui.ss")) - (define mred-launcher-names - (list "PLT Web Server"))) + (list "PLT Web Server"))) \ No newline at end of file diff --git a/collects/web-server/private/launch-gui.ss b/collects/web-server/private/gui.ss similarity index 100% rename from collects/web-server/private/launch-gui.ss rename to collects/web-server/private/gui.ss diff --git a/collects/web-server/private/launch-text.ss b/collects/web-server/private/main.ss similarity index 100% rename from collects/web-server/private/launch-text.ss rename to collects/web-server/private/main.ss