From 794923a997263e3c9445624e101bbfed4c104fcb Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sun, 20 Feb 2022 04:50:04 +0800 Subject: [PATCH] fix: update Unicode.lean --- lakefile.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index d0af360..cc8dd0e 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -11,7 +11,7 @@ package «doc-gen4» { }, { name := `Unicode - src := Source.git "https://github.com/xubaiw/Unicode.lean" "88ad4aacfcc7ab941a22c54de3e4fef0809cda87" + src := Source.git "https://github.com/xubaiw/Unicode.lean" "3b7b85472d42854a474099928a3423bb97d4fa64" } ] }