From f9bec769243203e0226fc2a5fefb734e977c3f00 Mon Sep 17 00:00:00 2001 From: John Benediktsson Date: Wed, 29 Jun 2022 09:45:29 -0700 Subject: [PATCH] help.html: round other colored boxes --- basis/help/html/html.factor | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/basis/help/html/html.factor b/basis/help/html/html.factor index 6a022d6178b..2915c9605b7 100644 --- a/basis/help/html/html.factor +++ b/basis/help/html/html.factor @@ -141,7 +141,11 @@ M: pathname url-of ] re-replace-with { "font-family: monospace;" "background-color:" } [ over subseq? ] all? [ - " border: 1px solid #e3e2db; border-radius: 5px; margin: 10px 0px;" append + " border: 1px solid #e3e2db; margin: 10px 0px;" append + ] when + + { "border:" "background-color:" } [ over subseq? ] all? [ + " border-radius: 5px;" append ] when ; : fix-help-header ( classes -- classes )