From 70e01755756b14a162256c92cd0d23858a6994a4 Mon Sep 17 00:00:00 2001 From: rhi Date: Sat, 4 Nov 2023 08:39:52 -0400 Subject: [PATCH] link to ascii syntax --- Home.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Home.md b/Home.md index dced207..33a8905 100644 --- a/Home.md +++ b/Home.md @@ -1,5 +1,7 @@ \*quox noise* +- if you don't feel like entering all those weird symbols, or you don't have an easy way to do so, an [[ascii syntax]] is also available + ## misc notes - [[agda w-type stuff]] \ No newline at end of file