Show error code in diagnostic header

2022-01-25 15:23:58 +01:00
parent ec0ca2a1b6
commit 7e55353de8
4 changed files with 29 additions and 13 deletions
@@ -264,6 +264,7 @@ path = { extends = "$text.2", size = 14, margin.left = 12 }
 background = "$state.active_line"
 border = { width = 1, top = true, bottom = true, color = "$border.0" }
 text = { extends = "$text.1", size = 14 }
+code = { extends = "$text.2", size = 14, margin.left = 10 }
 icon = { width = 10, margin.right = 8 }

 [editor.diagnostic_header.highlighted_text]