Summary
- merged
- tuned messages;
- NEWS;
- proper profiling within command execution: messages require PIDE id;
- more systematic treatment of profiling mode;
- tuned message;
- prefer less intrusive tracing message;
- clarified documentation: tracing messages are not shown here;
- add missing file;
- more formal ML profiling messages;
- clarified modules;