Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned;
  2. proper fonts (cf. 1d219d76873b);
  3. all_known can cause timeout of VSCode server startup, notably on Windows;
  4. tuned documentation; updated package version; updated screenshot reference;
Changeset 66243:453f9cabddb5 by wenzelm:
tuned;
The file was modified src/Pure/Thy/sessions.scala (diff)
Changeset 66242:a912f4a701bf by wenzelm:
proper fonts (cf. 1d219d76873b);
The file was modified Admin/lib/Tools/makedist (diff)
Changeset 66241:8f39d60b943d by wenzelm:
all_known can cause timeout of VSCode server startup, notably on Windows;
The file was modified src/Tools/VSCode/src/server.scala (diff)
Changeset 66240:1a04946c41d6 by wenzelm:
tuned documentation;<br>updated package version;<br>updated screenshot reference;
The file was modified src/Tools/VSCode/extension/README.md (diff)
The file was modified src/Tools/VSCode/extension/package.json (diff)