more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
more Document_Build.running_script, but display it as "Running XYZ";
Description
Description
Details
Details
- Provenance
makarius Authored on - Parents
- rISABELLEa6d147b22b9b: clarified documentation: avoid odd speculations about PIDE;
- Branches
- Unknown
- Tags