From 17b60aeaafbc863c9d90a642135368167404edfb Mon Sep 17 00:00:00 2001 From: gabrielhdt <gabrielhondet@gmail.com> Date: Wed, 4 Mar 2020 14:33:25 +0100 Subject: [PATCH] newline for table? --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index c28a43b..a364c0e 100644 --- a/README.md +++ b/README.md @@ -44,6 +44,7 @@ The code of `set-local-abbrevs` comes from ``` And we define the following abbreviations, + |----------|---| | subtype | ⊑ | | upcast | ↑ | -- GitLab