diff --git a/content/blog/06_spa_agda_cfg/index.md b/content/blog/06_spa_agda_cfg/index.md
index 256f615..668618b 100644
--- a/content/blog/06_spa_agda_cfg/index.md
+++ b/content/blog/06_spa_agda_cfg/index.md
@@ -130,7 +130,7 @@ by one, leading to another `suc n` in the final type. This makes sense because i
 
 Here's my definition of `Graph`s written using `Fin`:
 
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 24 39 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 23 38 >}}
 
 I explicitly used a `size` field, which determines how many nodes are in the
 graph, and serves as the upper bound for the edge indices. From there, an
@@ -176,7 +176,7 @@ we will connect each of the outputs of one to each of the inputs of the other.
 
 This is defined by the operation `g₁ ↦ g₂`, which sequences two graphs `g₁` and `g₂`:
 
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 72 83 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 71 82 >}}
 
 The definition starts out pretty innocuous, but gets a bit complicated by the
 end. The sum of the numbers of nodes in the two operands becomes the new graph
@@ -238,7 +238,7 @@ operation when combining the sub-CFGs of the "if" and "else" branches of an
 `if`/`else`, which both follow the condition, and both proceed to the code after
 the conditional.
 
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 59 70 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 58 69 >}}
 
 Everything here is just concatenation; we pool together the nodes, edges,
 inputs, and outputs, and the main source of complexity is the re-indexing.
@@ -250,12 +250,12 @@ from the graph for `while` loops I showed above; the reason for that is that
 I currently don't include the conditional expressions in my CFG. This is a
 limitation that I will address in future work.
 
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 85 95 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 84 94 >}}
 
 Given these thee operations, I construct Control Flow Graphs as follows, where
 `singleton` creates a new CFG node with the given list of simple statements:
 
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 122 126 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 121 125 >}}
 
 Throughout this, I've been liberal to include empty CFG nodes as was convenient.
 This is a departure from the formal definition I gave above, but it makes
diff --git a/data/submodules.json b/data/submodules.json
index 9d5328d..538300f 100644
--- a/data/submodules.json
+++ b/data/submodules.json
@@ -1,5 +1,5 @@
 {
-  "agda-spa": "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/828b652d3b9266e27ef7cf5a8a7fb82e3fd3133f",
+  "agda-spa": "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/913121488069a20cdfd40777a8777eb3744c415e",
   "aoc-2020": "https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020/src/commit/7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82",
   "blog-static-flake": "https://dev.danilafe.com/Nix-Configs/blog-static-flake/src/commit/67b47d9c298e7476c2ca211aac5c5fd961637b7b",
   "compiler": "https://dev.danilafe.com/DanilaFe/bloglang/src/commit/137455b0f4365ba3fd11c45ce49781cdbe829ec3",