From f872fffbbf4cf66851145edb65a65d1f780d221b Mon Sep 17 00:00:00 2001 From: "Narazaki, Shuji" Date: Thu, 2 Jan 2025 11:29:08 +0900 Subject: [PATCH] Update README.md --- README.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index f0d1ed0..c7d0778 100644 --- a/README.md +++ b/README.md @@ -5,8 +5,8 @@ ## How to type unicode symbols in -- Use simple-completion extension -- Use snippet (CONFIG/snippets/lean4.json) like this: +- Use simple-completion extension (But I don't know how to configure it) +- Use snippet (CONFIG/snippets/lean4.json) like this (But a newline is inserted after completion): ```json {