Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. no tracing SPAM, and thus more visible warnings;
  2. moved getopts to Scala;
  3. tuned messages;
  4. more operations (like Markup.parse_bool in ML);
  5. tuned messages;
  6. support for command-line options as in GNU bash;
Changeset 62436:beb3e6c1fa5a by wenzelm:
no tracing SPAM, and thus more visible warnings;
The file was modified src/HOL/Import/import_rule.ML (diff)
Changeset 62435:2c390ad93bc8 by wenzelm:
moved getopts to Scala;
The file was modified Admin/lib/Tools/build_doc (diff)
The file was modified src/Pure/Tools/build_doc.scala (diff)
Changeset 62434:4630b1748cb3 by wenzelm:
tuned messages;
The file was modified src/Pure/System/getopts.scala (diff)
Changeset 62433:2436a02f28c4 by wenzelm:
more operations (like Markup.parse_bool in ML);
The file was modified src/Pure/General/properties.scala (diff)
Changeset 62432:183c319b26dc by wenzelm:
tuned messages;
The file was modified src/Pure/System/getopts.scala (diff)
Changeset 62431:fbccea37091d by wenzelm:
support for command-line options as in GNU bash;
The file was addedsrc/Pure/System/getopts.scala
The file was modified src/Pure/build-jars (diff)