[chore]: Delete useless $

follow up on Guldoman's comment
2022-07-13 09:16:32 +02:00
parent 030dcc1e62
commit 7f9287a7e7
7 changed files with 7 additions and 7 deletions
@@ -12,7 +12,7 @@ syntax.add {
    { pattern = { "'", "'", '\\' },          type = "string" },
    { pattern = { "%[%[", "%]%]" },          type = "string" },
    { pattern = { "%-%-%[%[", "%]%]"},       type = "comment" },
-    { pattern = "%-%-.*$",                   type = "comment" },
+    { pattern = "%-%-.*",                    type = "comment" },
    { pattern = "0x%x+%.%x*[pP][-+]?%d+",    type = "number" },
    { pattern = "0x%x+%.%x*",                type = "number" },
    { pattern = "0x%.%x+[pP][-+]?%d+",       type = "number" },