grammars/source.lean.json in github-linguist-7.10.0 vs grammars/source.lean.json in github-linguist-7.11.0

@@ -127,10 +127,13 @@
       "name": "comment.block.lean",
       "begin": "/-",
       "end": "-/",
       "patterns": [
         {
+          "include": "source.lean.markdown"
+        },
+        {
           "include": "#blockComment"
         }
       ]
     },
     "comments": {
@@ -140,10 +143,13 @@
         },
         {
           "include": "#docComment"
         },
         {
+          "include": "#stringBlock"
+        },
+        {
           "include": "#modDocComment"
         },
         {
           "include": "#blockComment"
         }
@@ -151,10 +157,15 @@
     },
     "dashComment": {
       "name": "comment.line.double-dash.lean",
       "begin": "(--)",
       "end": "$",
+      "patterns": [
+        {
+          "include": "source.lean.markdown"
+        }
+      ],
       "beginCaptures": {
         "0": {
           "name": "punctuation.definition.comment.lean"
         }
       }
@@ -187,9 +198,22 @@
     },
     "modDocComment": {
       "name": "comment.block.documentation.lean",
       "begin": "/-!",
       "end": "-/",
+      "patterns": [
+        {
+          "include": "source.lean.markdown"
+        },
+        {
+          "include": "#blockComment"
+        }
+      ]
+    },
+    "stringBlock": {
+      "name": "comment.block.string.lean",
+      "begin": "/-\"",
+      "end": "\"-/",
       "patterns": [
         {
           "include": "source.lean.markdown"
         },
         {