From f662ea53225f7f04a9464b9845c5306867bbf52a Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Wed, 19 Jan 2011 06:32:01 -0700 Subject: [PATCH] DrRacket printing: disable date and filename banner --- collects/drracket/private/unit.rkt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/collects/drracket/private/unit.rkt b/collects/drracket/private/unit.rkt index 526750aa30..9354c1144d 100644 --- a/collects/drracket/private/unit.rkt +++ b/collects/drracket/private/unit.rkt @@ -752,8 +752,8 @@ module browser threading seems wrong. (define/override (on-paint before dc left top right bottom dx dy draw-caret) (super on-paint before dc left top right bottom dx dy draw-caret) - ;; For printing, put date and filename in the top margin: - (when (and before (is-printing?)) + ;; [Disabled] For printing, put date and filename in the top margin: + (when (and #f before (is-printing?)) (let ([h (box 0)] [w (box 0)]) (send (current-ps-setup) get-editor-margin w h)