Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
Changeset 68491:f0f83ce0badd by wenzelm:
disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
The file was modified etc/options (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Tools/dump.scala (diff)