Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. proper treatment of process_result;
  2. more accurate process_result in ML, corresponding to Process_Result in Scala;
  3. clarified: proper trim_line for error;
  4. unused;
Changeset 73269:f5a77ee9106c by wenzelm:
proper treatment of process_result;
The file was modified src/HOL/Tools/Quickcheck/narrowing_generators.ML (diff)
Changeset 73268:c8abfe393c16 by wenzelm:
more accurate process_result in ML, corresponding to Process_Result in Scala;
The file was modified src/Pure/System/bash.scala (diff)
The file was modified src/Pure/System/isabelle_system.ML (diff)
Changeset 73267:1d610d5524ff by wenzelm:
clarified: proper trim_line for error;
The file was modified src/Pure/Tools/ghc.ML (diff)
Changeset 73266:d6a664daa285 by wenzelm:
unused;
The file was removedsrc/Pure/System/kill.ML