Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. provide index.html; tuned;
  2. cpu time is optional (see Timing.message_resources);
  3. proper display of "_";
  4. clarified options and arguments; tuned;
Changeset 63703:ec095a532a2b by wenzelm:
provide index.html;<br>tuned;
The file was modified src/Pure/Tools/build_stats.scala (diff)
Changeset 63702:fed1d4dab990 by wenzelm:
cpu time is optional (see Timing.message_resources);
The file was modified src/Pure/Tools/build_stats.scala (diff)
Changeset 63701:3744d2cf4d2f by wenzelm:
proper display of &quot;_&quot;;
The file was modified src/Pure/Tools/build_stats.scala (diff)
Changeset 63700:2a95d904672e by wenzelm:
clarified options and arguments;<br>tuned;
The file was modified src/Pure/General/time.scala (diff)
The file was modified src/Pure/Tools/build_stats.scala (diff)