From e2e5371e142562d913441ddee8d605dcd717ef01 Mon Sep 17 00:00:00 2001 From: Zumi Daxuya Date: Tue, 12 Sep 2023 09:42:07 +0700 Subject: [PATCH] docpdf: add dot leaders in ToC --- res/docpdf/make_paper.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/res/docpdf/make_paper.py b/res/docpdf/make_paper.py index 79971b0cd..83dc966e9 100644 --- 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;