Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. backout 930a30c1a9af: leads to odd effect of command-line options becoming persistent preferences;
  2. eliminated ancient TTY-based Tactical.tracify and related global references;
  3. updated according to 705d4c4003ea;
Changeset 62917:eed66ba99bd9 by wenzelm:
backout 930a30c1a9af: leads to odd effect of command-line options becoming persistent preferences;
The file was modified src/Doc/JEdit/JEdit.thy (diff)
The file was modified src/Tools/jEdit/lib/Tools/jedit (diff)
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
Changeset 62916:621afc4607ec by wenzelm:
eliminated ancient TTY-based Tactical.tracify and related global references;
The file was modified src/Pure/search.ML (diff)
The file was modified src/Pure/tactical.ML (diff)
Changeset 62915:0f794993485a by wenzelm:
updated according to 705d4c4003ea;
The file was modified Admin/Release/build_library (diff)