From 08dbf239a6f7f6506fe331fbed6d6b94acbb4ea3 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 10 Oct 2021 11:24:17 +0200
Subject: [PATCH] chore: server: redundant let

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

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index beb9f33426..2c09ab6a37 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -146,9 +146,8 @@ section Initialization
       -- ignore any output up to the last line
       -- TODO: leanpkg should instead redirect nested stdout output to stderr
       let stdout := stdout.split (· == '\n') |>.getLast!
-      let Except.ok paths ← pure (Json.parse stdout >>= fromJson?)
+      let Except.ok (paths : LeanPaths) ← pure (Json.parse stdout >>= fromJson?)
         | throwServerError s!"invalid output from `{cmdStr}`:\n{stdout}\nstderr:\n{stderr}"
-      let paths : LeanPaths ← IO.ofExcept <| fromJson? paths
       let sp ← getBuiltinSearchPath
       let sp ← addSearchPathFromEnv sp
       let sp := paths.oleanPath ++ sp