Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. meta_digest without accidental source positions (amending 1544e61e5314): avoid spurious rebuild of unrelated sessions after editing ROOT;
Changeset 65580:66351f79c295 by wenzelm:
meta_digest without accidental source positions (amending 1544e61e5314): avoid spurious rebuild of unrelated sessions after editing ROOT;
The file was modified src/Pure/Thy/sessions.scala (diff)