Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more options;
  2. allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
  3. tuned;
  4. tuned signature;
Changeset 67853:74e2a4b62826 by wenzelm:
more options;
The file was modified src/Pure/Tools/server_commands.scala (diff)
Changeset 67852:f701a1d5d852 by wenzelm:
allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Thy/thy_resources.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)
Changeset 67851:5e6452a6ec89 by wenzelm:
tuned;
The file was modified src/Tools/VSCode/src/protocol.scala (diff)
Changeset 67850:3e9fe7a84b5d by wenzelm:
tuned signature;
The file was modified src/Pure/General/json.scala (diff)
The file was modified src/Pure/Tools/server.scala (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)
The file was modified src/Tools/VSCode/src/protocol.scala (diff)