Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. suppress nodes with vacuous status, notably empty nodes (amending 5f160df596c1);
  2. tuned;
  3. more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
Changeset 69820:dfc5f8294fbc by wenzelm:
suppress nodes with vacuous status, notably empty nodes (amending 5f160df596c1);
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)
Changeset 69819:32c4f01a5e33 by wenzelm:
tuned;
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)
Changeset 69818:60d0ee8f2ddb by wenzelm:
more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
The file was modified src/Pure/PIDE/document_status.scala (diff)
The file was modified src/Pure/PIDE/headless.scala (diff)
The file was modified src/Pure/System/progress.scala (diff)
The file was modified src/Pure/Tools/server.scala (diff)
The file was modified src/Tools/jEdit/src/theories_dockable.scala (diff)