provide --baseImagesUrl for VSCode extensions marketplace;
authorwenzelm
Thu, 29 Jun 2017 23:05:58 +0200
changeset 66228 5707cfb531ee
parent 66227 7470985f3fb6
child 66229 d3b6e5e47015
provide --baseImagesUrl for VSCode extensions marketplace;
src/Tools/VSCode/src/build_vscode.scala
--- a/src/Tools/VSCode/src/build_vscode.scala	Thu Jun 29 23:05:33 2017 +0200
+++ b/src/Tools/VSCode/src/build_vscode.scala	Thu Jun 29 23:05:58 2017 +0200
@@ -36,7 +36,10 @@
     progress.echo(output_path.implode)
 
     progress.bash(
-      "npm install && npm update --dev && vsce " + (if (publish) "publish" else "package"),
+      "npm install && npm update --dev && vsce " +
+      (if (publish)
+        "publish --baseImagesUrl http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/Tools/VSCode/extension"
+       else "package"),
       cwd = extension_dir.file, echo = true).check
   }