#339 (May 30, 2017, 12:50:08 AM)

1. merged (detail / hgweb)
2. update preview after document change;
   clarified encode_name/decode_name;
   clarified other_column; (detail / hgweb)
3. proper HTML preview; (detail / hgweb)
4. clarified view column;
   tuned whitespace; (detail / hgweb)
5. basic setup for document preview; (detail / hgweb)
6. Tuned Library/Sublist.thy (detail / hgweb)
7. reorganised material on sublists (detail / hgweb)

Started by an SCM change

This run spent:

• 6.9 sec waiting;
• 1 hr 20 min build duration;
• 1 hr 21 min total from scheduled to completion.