From 3ceb6f10519491dbfc1d44177010b1bc18afc159 Mon Sep 17 00:00:00 2001 From: John Benediktsson Date: Tue, 26 Jul 2022 01:38:07 -0700 Subject: [PATCH] ui.theme.base16: adding code-border-color --- basis/ui/theme/base16/base16.factor | 1 + 1 file changed, 1 insertion(+) diff --git a/basis/ui/theme/base16/base16.factor b/basis/ui/theme/base16/base16.factor index 2b0231d33b..ab3d424e2f 100644 --- a/basis/ui/theme/base16/base16.factor +++ b/basis/ui/theme/base16/base16.factor @@ -77,6 +77,7 @@ M: base16-theme deprecated-border-color "base01" named-base16 ; M: base16-theme warning-background-color "base01" named-base16 ; M: base16-theme warning-border-color "base01" named-base16 ; M: base16-theme code-background-color "base01" named-base16 ; +M: base16-theme code-border-color "base01" named-base16 ; M: base16-theme help-path-border-color "base00" named-base16 ; M: base16-theme tip-background-color "base01" named-base16 ; -- 2.34.1