Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. avoid spurious output after exit;
  2. updated package version;
  3. proper state_panel exit;
Changeset 66397:f55d2e2c2ca0 by wenzelm:
avoid spurious output after exit;
The file was modified src/Tools/VSCode/src/state_panel.scala (diff)
Changeset 66396:29717b0a1ab3 by wenzelm:
updated package version;
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 66395:14146fb264d8 by wenzelm:
proper state_panel exit;
The file was modified src/Tools/VSCode/extension/src/extension.ts (diff)
The file was modified src/Tools/VSCode/extension/src/state_panel.ts (diff)