From 0c716e4c6b7c2c44bbfd02b6503cae66af7b7480 Mon Sep 17 00:00:00 2001 From: Marshall Lochbaum Date: Fri, 28 Jan 2022 16:34:41 -0500 Subject: Separate syntax highlighting category for header/body characters ;:? --- docs/help/nothing.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'docs/help/nothing.html') diff --git a/docs/help/nothing.html b/docs/help/nothing.html index 09188be2..b83a26c4 100644 --- a/docs/help/nothing.html +++ b/docs/help/nothing.html @@ -17,7 +17,7 @@

In Block Headers

For Block header pattern matching syntax, Nothing can be used to indicate an unused value.

-↗️
    F  {𝕊 a·b: ab}
+↗️
    F  {𝕊 a·b: ab}
 
     F 123
 ⟨ 1 3 ⟩
-- 
cgit v1.2.3