Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. clarified modules;
  2. tuned signature;
  3. tuned;
  4. proper Option.Spec.toString for bash script: avoid Token.quote_name of Options.Spec.print_value (amending 3d1746a716fa, see also 39f6f180008d);
Changeset 78911:81dab48582c6 by wenzelm:
clarified modules;
The file was modified src/Pure/System/options.scala (diff)
The file was modified src/Pure/Tools/build_cluster.scala (diff)
Changeset 78910:d305af09fbad by wenzelm:
tuned signature;
The file was modified src/Pure/System/bash.scala (diff)
Changeset 78909:65acbafc70e5 by wenzelm:
tuned;
The file was modified src/Pure/System/options.scala (diff)
Changeset 78908:f38153e58f21 by wenzelm:
proper Option.Spec.toString for bash script: avoid Token.quote_name of Options.Spec.print_value (amending 3d1746a716fa, see also 39f6f180008d);
The file was modified src/Pure/System/benchmark.scala (diff)
The file was modified src/Pure/System/options.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)