#1847 (Dec 27, 2022, 2:04:04 AM)

1. tuned signature; (detail / hgweb)
2. merged (detail / hgweb)
3. tuned signature; (detail / hgweb)
4. more robust; (detail / hgweb)
5. clarified signature: more position information via node_name; (detail / hgweb)
6. tuned signature: avoid name confusion; (detail / hgweb)
7. more bibtex errors;
   clarified Bibtex.Chunk.is_malformed (again): see also 9c1389befa56 and 7ee248f19ca9; (detail / hgweb)
8. clarified signature: internalize errors (but: the parser rarely fails); (detail / hgweb)
9. tuned signature; (detail / hgweb)
10. clarified signature: more explicit types; (detail / hgweb)
11. clarified buffer_state: not synchronized, but exclusively owned by GUI thread; (detail / hgweb)
12. merged (detail / hgweb)
13. removed old lemma names (detail / hgweb)

Started by an SCM change

This run spent:

• 1 hr 14 min waiting;
• 1 hr 51 min build duration;
• 3 hr 5 min total from scheduled to completion.