Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified defaults;
  2. tuned whitespace;
  3. tuned;
  4. clarified defaults;
  5. more operations;
  6. tuned signature;
Changeset 65056:002b4c8c366e by wenzelm:
clarified defaults;
The file was modified NEWS (diff)
The file was modified etc/options (diff)
The file was modified src/Pure/Admin/ci_profile.scala (diff)
Changeset 65055:12189e86c49d by wenzelm:
tuned whitespace;
The file was modified NEWS (diff)
Changeset 65054:9ad3f65c03f4 by wenzelm:
tuned;
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 65053:460f0fd2f77a by wenzelm:
clarified defaults;
The file was modified src/Pure/Tools/ml_statistics.scala (diff)
The file was modified src/Tools/jEdit/src/monitor_dockable.scala (diff)
Changeset 65052:7f825cc6debf by wenzelm:
more operations;
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 65051:f094e27e4902 by wenzelm:
tuned signature;
The file was modified src/Pure/Tools/ml_statistics.scala (diff)