diff -r 7470985f3fb6 -r 5707cfb531ee 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 }