Merge pull request #1477 from ZoomTen/docs-3

docpdf: add dot leaders in ToC
2023-09-11 21:50:09 -05:00 · 2023-09-11 21:50:09 -05:00 · cdb1638cb3
parent e88d3b8483 e2e5371e14
commit cdb1638cb3
1 changed files with 2 additions and 1 deletions
--- a/res/docpdf/make_paper.py
+++ b/res/docpdf/make_paper.py
@ -227,7 +227,8 @@ if __name__ == "__main__":
            letter-spacing: .01em;
          }
          a.indexItemPre[href^='#']:after {
-            content: '';
+            content: ' ' leader('.') ' ';
+            font-size: 1em;
          }
          a.indexItem {
            float: right;