Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper order;
  2. clarified README;
  3. merged
  4. more ssh options;
  5. support for proxy connection, similar to ProxyCommand in ssh config;
  6. prefer https;
  7. avoid hardwired parameters; less ambitious defaults: low memory requirements;
  8. Drop illegitimate optimisation from d5a7f2c54655.
  9. Fall back to reading rewrite morphism first if activation fails without it.
  10. Proper rewrite morphisms in locale instances.
Changeset 67749:08dc76bf6400 by wenzelm:
proper order;
The file was modified src/Pure/Admin/build_status.scala (diff)
Changeset 67748:94a8fddc1e7c by wenzelm:
clarified README;
The file was modified Admin/cronjob/README (diff)
The file was removedAdmin/build_log/README
Changeset 67747:7b84ecd54d70 by wenzelm:
merged
Changeset 67746:cb0f0f5f8876 by wenzelm:
more ssh options;
The file was modified src/Pure/Admin/isabelle_cronjob.scala (diff)
Changeset 67745:d83efbe52438 by wenzelm:
support for proxy connection, similar to ProxyCommand in ssh config;
The file was modified src/Pure/General/ssh.scala (diff)
Changeset 67744:5c781dcd5864 by wenzelm:
prefer https;
The file was modified Admin/cronjob/plain_identify (diff)
The file was modified Admin/cronjob/self_update (diff)
The file was modified README_REPOSITORY (diff)
The file was modified src/Doc/Implementation/ML.thy (diff)
The file was modified src/Pure/Admin/build_history.scala (diff)
The file was modified src/Tools/VSCode/extension/README.md (diff)
The file was modified src/Tools/VSCode/extension/package.json (diff)
Changeset 67743:7bd0a250183b by wenzelm:
avoid hardwired parameters;<br>less ambitious defaults: low memory requirements;
The file was modified etc/options (diff)
The file was modified src/Pure/Admin/build_log.scala (diff)
Changeset 67742:6306bd582957 by ballarin:
Drop illegitimate optimisation from d5a7f2c54655.
The file was modified src/Pure/Isar/expression.ML (diff)
Changeset 67741:d5a7f2c54655 by ballarin:
Fall back to reading rewrite morphism first if activation fails without it.
The file was modified NEWS (diff)
The file was modified src/Pure/Isar/expression.ML (diff)
Changeset 67740:b6ce18784872 by ballarin:
Proper rewrite morphisms in locale instances.
The file was modified NEWS (diff)
The file was modified src/Doc/Isar_Ref/Spec.thy (diff)
The file was modified src/FOL/ex/Locale_Test/Locale_Test1.thy (diff)
The file was modified src/Pure/Isar/element.ML (diff)
The file was modified src/Pure/Isar/expression.ML (diff)
The file was modified src/Pure/Isar/interpretation.ML (diff)
The file was modified src/Pure/Isar/parse_spec.ML (diff)
The file was modified src/Pure/Pure.thy (diff)