Summary
- tuned -- fewer warnings;
- avoid old SML90;
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) |
The file was modified | src/Pure/General/exn.ML (diff) |
The file was modified | src/Pure/ML/ml_pervasive.ML (diff) |