From 352de1d2d7daf1adf1502384f6ca73b86c77443e Mon Sep 17 00:00:00 2001 From: jcs090218 <8685505+jcs090218@users.noreply.github.com> Date: Sun, 31 Aug 2025 02:02:43 +0000 Subject: [PATCH] chore: Bump agda grammar --- repos/agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/repos/agda b/repos/agda index b9b32fa04..e8d47a698 160000 --- a/repos/agda +++ b/repos/agda @@ -1 +1 @@ -Subproject commit b9b32fa042c2952a7bfca86847ea325e44ccc897 +Subproject commit e8d47a6987effe34d5595baf321d82d3519a8527