aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--ide/utf8.v (renamed from ide/notations.v)0
1 files changed, 0 insertions, 0 deletions
diff --git a/ide/notations.v b/ide/utf8.v
index d0d94dc518..d0d94dc518 100644
--- a/ide/notations.v
+++ b/ide/utf8.v