From ae2251fc7721a6c985351db06dbb0f66171c705f Mon Sep 17 00:00:00 2001
From: Silvus <s8bnpete@stud.uni-saarland.de>
Date: Thu, 25 Aug 2022 08:54:46 +0200
Subject: [PATCH] Fixed ilnk to iris/bi/ascii.v

---
 docs/editor.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/editor.md b/docs/editor.md
index cd9b19684..92ff9a3ee 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -5,7 +5,7 @@ If you really want to, you can also avoid having to type unicode characters by
 importing `iris.bi.ascii`.  That enables parsing-only ASCII alternatives to many
 unicode notations. (Feel free to report an issue when you notice that a notation
 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).
+[read this file](/iris/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. In particular,
-- 
GitLab