From fadbb0029c7b8b0625870301278a0c2628a88b71 Mon Sep 17 00:00:00 2001
From: toh995 <52012721+toh995@users.noreply.github.com>
Date: Tue, 16 Jun 2026 05:18:29 -0700
Subject: [PATCH] Fix local build output directory path in README

---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index f51ae094..df4521ec 100644
--- a/README.md
+++ b/README.md
@@ -10,5 +10,5 @@ The book's build has been tested with:
 1. Lean 4 (see the version in lean-toolchain in examples/)
 2. expect (tested with v5.45.4 but any version from the last decade should work)
 
-To build the book, change to the "book" directory and run "lake exe fp-lean". After this, "book/out/html-multi" contains a multi-page Web version of the book.
+To build the book, change to the "book" directory and run "lake exe fp-lean". After this, "book/_out/html-multi" contains a multi-page Web version of the book.