#1812 (Nov 8, 2022, 12:50:10 AM)

1. suppress document_required GUI element for now: still unused; (detail / hgweb)
2. clarified layout; (detail / hgweb)
3. clarified node_required status: distinguish theory_required vs. document_required;
   more robust and more correct Geometry.in operation; (detail / hgweb)

Started by an SCM change

This run spent:

• 9.4 sec waiting;
• 1 hr 51 min build duration;
• 1 hr 51 min total from scheduled to completion.