Summary
- no tracing SPAM, and thus more visible warnings;
- moved getopts to Scala;
- tuned messages;
- more operations (like Markup.parse_bool in ML);
- tuned messages;
- support for command-line options as in GNU bash;
The file was modified | src/HOL/Import/import_rule.ML (diff) |
The file was modified | Admin/lib/Tools/build_doc (diff) |
The file was modified | src/Pure/Tools/build_doc.scala (diff) |
The file was modified | src/Pure/System/getopts.scala (diff) |
The file was modified | src/Pure/General/properties.scala (diff) |
The file was modified | src/Pure/System/getopts.scala (diff) |
The file was added | src/Pure/System/getopts.scala |
The file was modified | src/Pure/build-jars (diff) |