Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. tuned;
  2. copy jEdit sources instead of jar, for better browsing experience;
  3. proper option;
Changeset 71525:d7b0d078266d by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src-base/dockable.scala (diff)
The file was modified src/Tools/jEdit/src/debugger_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/documentation_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/graphview_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/query_dockable.scala (diff)
The file was modified src/Tools/jEdit/src/sledgehammer_dockable.scala (diff)
Changeset 71524:4b908e70d642 by wenzelm:
copy jEdit sources instead of jar, for better browsing experience;
The file was modified src/Pure/Tools/scala_project.scala (diff)
Changeset 71523:abe3c309998b by wenzelm:
proper option;
The file was modified src/Doc/System/Scala.thy (diff)