From 04d223b9e1bc6e4bed2f31fc1127372df22fd954 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 15 Jul 2020 12:27:19 +0200
Subject: [PATCH] Unicode is required in Iris itself

---
 docs/editor.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/docs/editor.md b/docs/editor.md
index df25c9393..8658cbc2b 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -8,7 +8,9 @@ is missing.)  The easiest way to learn the ASCII syntax is to
 [read this file](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/theories/bi/ascii.v).
 Note however that this will make your code harder to read and work on for Iris
 developers that are used to our default unicode notation---generally, our
-recommendation is to use the unicode syntax whenever possible.
+recommendation is to use the unicode syntax whenever possible. In particular,
+Unicode syntax is required for MRs to Iris itself and other Iris-managed
+repositories.
 
 ## General: Unicode Fonts
 
-- 
GitLab