diff --git a/docs/editor.md b/docs/editor.md
index cd9b19684de0a3def18de0147e403928a0e1b2f4..92ff9a3ee30dfc3ced2fb82fa44959e199cf717d 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,