#1881 (Feb 4, 2023, 12:50:10 AM)

1. no view_document after build: avoid loss of focus, especially in "auto build" mode; (detail / hgweb)
2. tuned message; (detail / hgweb)
3. build only if required, view only after proper build: thus avoid pointless events in "auto build" mode; (detail / hgweb)
4. clarified modules; (detail / hgweb)
5. maintain document_output meta data; (detail / hgweb)
6. clarified modules; (detail / hgweb)
7. avoid redundant SelectionChanged events; (detail / hgweb)
8. more logging; (detail / hgweb)
9. proper symbolic handle on component resources:
   diff -r ci-extras-1/etc/settings ci-extras-2/etc/settings
   1c1,4
   < classpath "$COMPONENT/lib/ci-extras.jar"
   ---
   > #-*- shell-script -*- :mode=shellscript:
   >
   > ISABELLE_CI_EXTRAS_JAR="$COMPONENT/lib/ci-extras.jar"
   > classpath "$ISABELLE_CI_EXTRAS_JAR"
   diff -r ci-extras-1/README ci-extras-2/README
   11a12
   > Makarius, 02-Feb-2023 (detail / hgweb)
10. more robust on Windows, where C:\\ and \\SERVER\SHARE cause problems (line 920 of winbasicio.cpp); (detail / hgweb)

Started by an SCM change

This run spent:

• 8.4 sec waiting;
• 1 hr 52 min build duration;
• 1 hr 52 min total from scheduled to completion.