Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. proper File.platform_path for SML/NJ on Windows;
  3. clarified signature;
  4. proper output of raw ML;
Changeset 66784:df1f43d477f5 by wenzelm:
merged
Changeset 66783:bbe87f1b5e5d by wenzelm:
proper File.platform_path for SML/NJ on Windows;
The file was modified src/HOL/Library/code_test.ML (diff)
Changeset 66782:193c31b79a33 by wenzelm:
clarified signature;
The file was modified src/Pure/ML/ml_process.scala (diff)
The file was modified src/Pure/ML/ml_syntax.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 66781:dac4cfbfede8 by wenzelm:
proper output of raw ML;
The file was modified src/Pure/ML/ml_process.scala (diff)