#801 (Nov 28, 2018, 12:52:51 AM)

1. adjusted to fc221fa79741; (detail / hgweb)
2. obsolete (see fc221fa79741); (detail / hgweb)
3. adjusted to fc221fa79741; (detail / hgweb)
4. adjusted to Isabelle DejaVu fonts (see also 8bd8750a2f9b, b3c665940d62); (detail / hgweb)
5. more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
   tuned signature; (detail / hgweb)
6. more robust (amending 76979adf0b96); (detail / hgweb)
7. more robust: avoid broken YXML due to Markup.empty; (detail / hgweb)

Started by an SCM change

This run spent:

• 2 min 49 sec waiting;
• 1 hr 17 min build duration;
• 1 hr 19 min total from scheduled to completion.