Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified modules;
  2. more uniform JVM vs. ML status widget;
  3. clarified modules;
Changeset 72250:13976f92a2d0 by wenzelm:
clarified modules;
The file was addedsrc/Pure/System/java_statistics.scala
The file was modified src/Pure/ML/ml_statistics.scala (diff)
The file was modified src/Pure/System/platform.scala (diff)
The file was modified src/Pure/build-jars (diff)
The file was modified src/Tools/jEdit/src/status_widget.scala (diff)
Changeset 72249:4bf8a8a2d2ad by wenzelm:
more uniform JVM vs. ML status widget;
The file was modified NEWS (diff)
The file was modified src/Doc/JEdit/JEdit.thy (diff)
The file was modified src/Pure/System/platform.scala (diff)
The file was modified src/Tools/jEdit/src/jEdit.props (diff)
The file was modified src/Tools/jEdit/src/services.xml (diff)
The file was modified src/Tools/jEdit/src/status_widget.scala (diff)
Changeset 72248:71378e7d148e by wenzelm:
clarified modules;
The file was addedsrc/Tools/jEdit/src/status_widget.scala
The file was modified src/Tools/jEdit/lib/Tools/jedit (diff)
The file was modified src/Tools/jEdit/src/services.xml (diff)
The file was removedsrc/Tools/jEdit/src/ml_status.scala