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;
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)