Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. no censorship of view title;
  3. set view title dynamically;
  4. tuned
  5. tuned
Changeset 68082:b25ccd85b1fd by wenzelm:
merged
Changeset 68081:3d8f34715013 by wenzelm:
no censorship of view title;
The file was addedsrc/Tools/jEdit/patches/title
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
Changeset 68080:17f79ae49401 by wenzelm:
set view title dynamically;
The file was modified Admin/lib/Tools/makedist_bundle (diff)
The file was modified NEWS (diff)
The file was modified src/Tools/jEdit/src/jEdit.props (diff)
The file was modified src/Tools/jEdit/src/plugin.scala (diff)
Changeset 68079:9c2088adff8b by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Sorting.thy (diff)
Changeset 68078:48e188cb1591 by nipkow:
tuned
The file was modified src/HOL/Data_Structures/Sorting.thy (diff)