Summary
- backout 930a30c1a9af: leads to odd effect of command-line options becoming persistent preferences;
- eliminated ancient TTY-based Tactical.tracify and related global references;
- updated according to 705d4c4003ea;
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) |
The file was modified | src/Pure/search.ML (diff) |
The file was modified | src/Pure/tactical.ML (diff) |
The file was modified | Admin/Release/build_library (diff) |