From cf101fa5ae2e9ade0d258e55566b65d2581ff659 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 2 Jan 2021 23:45:25 +0100
Subject: [PATCH] chore: that last commit shouldn't have worked, and yet
 apparently it did

---
 src/Lean/Server/FileWorker.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 24a6c47f57..f0d8e4eb33 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -305,6 +305,7 @@ section RequestHandling
           match cmdSnaps with
           | AsyncList.asyncTail tl =>
             discard <| IO.wait tl
+            let ⟨cmdSnaps, _⟩ ← cmdSnaps.updateFinishedPrefix
             lastSnap? := cmdSnaps.finishedPrefix.getLast?
           | _ => ()
         if let some lastSnap := lastSnap? then