From eced37475628c314ce62671c59452ccd31ba2e02 Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Tue, 28 May 2002 18:09:27 +0000 Subject: [PATCH] .. original commit: 81b248af6bb651af48c2c0c0a9be2390f63580c4 --- collects/help/help.ss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/collects/help/help.ss b/collects/help/help.ss index 86900903..c52aa0eb 100644 --- a/collects/help/help.ss +++ b/collects/help/help.ss @@ -20,7 +20,7 @@ (lib "mred.ss" "mred")) (preferences:add-editor-checkbox-panel) - (preferences:add-misc-checkbox-panel) + (preferences:add-warnings-checkbox-panel) ;; don't call preferences:add-scheme-checkbox-panel ;; here since those prefs don't really apply to Help Desk (add-proxy-prefs-panel)