From 94dbfba0f3f77c9603bcba4aee249823cc91eeed Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Wed, 4 Jun 2014 13:34:03 +0100 Subject: [PATCH] scribble: fix `history` spacing --- .../scribble-lib/scribble/private/manual-history.rkt | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/pkgs/scribble-pkgs/scribble-lib/scribble/private/manual-history.rkt b/pkgs/scribble-pkgs/scribble-lib/scribble/private/manual-history.rkt index 994bc79862..05bda39b74 100644 --- a/pkgs/scribble-pkgs/scribble-lib/scribble/private/manual-history.rkt +++ b/pkgs/scribble-pkgs/scribble-lib/scribble/private/manual-history.rkt @@ -48,8 +48,9 @@ [i (in-naturals)]) (define vers (history-entry-vers e)) (list (if (zero? i) - "" - " ") + null + (list null ; needed to avoid " " dropped as whitespace + " ")) (history-entry-what e) " in version " vers