Skip to content
Success

Changes

Summary

  1. tuned -- fewer warnings;
  2. avoid old SML90;
Changeset 63926:70973a1b4ec0 by wenzelm:
tuned -- fewer warnings;
The file was modified src/Pure/Tools/build_stats.scala (diff)
The file was modified src/Pure/library.scala (diff)
The file was modified src/Tools/jEdit/src/symbols_dockable.scala (diff)
Changeset 63925:500646ef617a by wenzelm:
avoid old SML90;
The file was modified src/Pure/General/exn.ML (diff)
The file was modified src/Pure/ML/ml_pervasive.ML (diff)