From 27f3c73eacbeb99d8038e61ec46a9ff603ebbb29 Mon Sep 17 00:00:00 2001 From: Darcy Shen Date: Tue, 21 Nov 2023 15:46:30 +0800 Subject: [PATCH] [35][69] Several chore tasks --- devel/35.tm | 3 ++- devel/69.tm | 4 +++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/devel/35.tm b/devel/35.tm index c05123c8f2..4146cbc247 100644 --- a/devel/35.tm +++ b/devel/35.tm @@ -9,7 +9,8 @@ ||||>|>|||>|>>>> + icon in contextual help template>>|||>|>>>> diff --git a/devel/69.tm b/devel/69.tm index 68a53a751b..af838c3ffe 100644 --- a/devel/69.tm +++ b/devel/69.tm @@ -13,7 +13,9 @@ do not use italic font for the render-theorem body>>|||>|>||>|>|>>>> + encoding to include a file with unicode + filename>>|||>|Compare with from being translated>>>>>