# HG changeset patch # User Thomas Lindae # Date 1720208439 -7200 # Node ID c87d2fa560ddf49f601da9794acea84aa1980bbf # Parent 2ab384664ac571f64e6be8382b0685961f2b8264 vscode: changed how options are inserted into package.json so that one can still call `npm install` without errors; diff -r 2ab384664ac5 -r c87d2fa560dd src/Tools/VSCode/extension/package.json --- a/src/Tools/VSCode/extension/package.json Fri Jul 05 13:30:07 2024 +0200 +++ b/src/Tools/VSCode/extension/package.json Fri Jul 05 21:40:39 2024 +0200 @@ -193,7 +193,7 @@ "configuration": { "title": "Isabelle", "properties": { - /*options*/ + "ISABELLE_OPTIONS": {}, "isabelle.replacement": { "type": "string", "default": "non-alphanumeric", diff -r 2ab384664ac5 -r c87d2fa560dd src/Tools/VSCode/src/component_vscode_extension.scala --- a/src/Tools/VSCode/src/component_vscode_extension.scala Fri Jul 05 13:30:07 2024 +0200 +++ b/src/Tools/VSCode/src/component_vscode_extension.scala Fri Jul 05 21:40:39 2024 +0200 @@ -231,7 +231,7 @@ val opt_json = options_json(options) val package_path = build_dir + Path.basic("package.json") - val package_body = File.read(package_path).replace("/*options*/", opt_json) + val package_body = File.read(package_path).replace("\"ISABELLE_OPTIONS\": {},", opt_json) File.write(package_path, package_body)