Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. regular user tool;
  2. avoid deprecated Scala;
Changeset 64342:53fb4a19fb98 by wenzelm:
regular user tool;
The file was addedsrc/Pure/Tools/profiling_report.scala
The file was modified NEWS (diff)
The file was modified src/Pure/build-jars (diff)
The file was removedsrc/Pure/Admin/profiling_report.scala
Changeset 64341:45b6faeee56d by wenzelm:
avoid deprecated Scala;
The file was modified src/Pure/Admin/build_log.scala (diff)