Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified name to avoid duplication (no distinction of data on host = lrzcloud2);
  2. clarified names;
  3. more errors;
Changeset 72074:f3e1144a1cec by wenzelm:
clarified name to avoid duplication (no distinction of data on host = lrzcloud2);
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 72073:f56522a44564 by wenzelm:
clarified names;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 72072:fed7b0ae20d8 by wenzelm:
more errors;
The file was modified src/Pure/PIDE/resources.scala (diff)