Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. some HTML GUI elements;
  3. proper bootstrap_name (amending b42743f5b595);
  4. clarified indentation;
Changeset 66197:c8604c9f3a8a by wenzelm:
merged
Changeset 66196:31c9b09cc1d4 by wenzelm:
some HTML GUI elements;
The file was modified src/Pure/PIDE/xml.scala (diff)
The file was modified src/Pure/Thy/html.scala (diff)
Changeset 66195:bb886f13623a by wenzelm:
proper bootstrap_name (amending b42743f5b595);
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/Thy/sessions.scala (diff)
The file was modified src/Pure/Thy/thy_header.scala (diff)
The file was modified src/Tools/VSCode/src/vscode_resources.scala (diff)
The file was modified src/Tools/jEdit/src/jedit_resources.scala (diff)
Changeset 66194:8d34d42c40cb by wenzelm:
clarified indentation;
The file was modified src/Pure/Pure.thy (diff)