Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. minor performance tuning, notably for Library.fold_string etc.;
  2. clarified file name;
  3. purge log files -- avoid old errors;
  4. expose bibtex errors;
Changeset 67206:b8f30228a55b by wenzelm:
minor performance tuning, notably for Library.fold_string etc.;
The file was modified src/Pure/ML/ml_init.ML (diff)
Changeset 67205:06c91eac25f2 by wenzelm:
clarified file name;
The file was addedsrc/Pure/ML/ml_init.ML
The file was modified src/Pure/ROOT.ML (diff)
The file was removedsrc/Pure/ML/ml_pervasive.ML
Changeset 67204:849a838f7e57 by wenzelm:
purge log files -- avoid old errors;
The file was modified src/Pure/Thy/present.scala (diff)
Changeset 67203:85784e16bec8 by wenzelm:
expose bibtex errors;
The file was modified NEWS (diff)
The file was modified src/Pure/Thy/present.scala (diff)
The file was modified src/Pure/Tools/bibtex.scala (diff)