Update mk_bundle.py

mmew-2022 · web-flow · commit 42fcf32d05c7 · 2023-01-15T23:00:08.000-05:00
diff --git a/mk_bundle.py b/mk_bundle.py
@@ -192,7 +192,7 @@ def get_lean_extension():
             "**/.DS_Store": true,
             "**/*.olean": true
         },
-        "lean.executablePath": "%extensionPath%/../../../../lean/bin/lean"
+        "lean.executablePath": "%extensionPath%/../../../../lean/bin/lean",
         "editor.minimap.enabled": false,
         "window.titleBarStyle": "custom",
     }

Original file line number	Diff line number	Diff line change
`@@ -192,7 +192,7 @@ def get_lean_extension():`
`192`	`192`	`"**/.DS_Store": true,`
`193`	`193`	`"*/.olean": true`
`194`	`194`	`},`
`195`		`- "lean.executablePath": "%extensionPath%/../../../../lean/bin/lean"`
	`195`	`+ "lean.executablePath": "%extensionPath%/../../../../lean/bin/lean",`
`196`	`196`	`"editor.minimap.enabled": false,`
`197`	`197`	`"window.titleBarStyle": "custom",`
`198`	`198`	`}`