Skip to content

Fix local build output directory path in README#277

Open
toh995 wants to merge 1 commit into
leanprover:masterfrom
toh995:patch-1
Open

Fix local build output directory path in README#277
toh995 wants to merge 1 commit into
leanprover:masterfrom
toh995:patch-1

Conversation

@toh995

@toh995 toh995 commented Jun 16, 2026

Copy link
Copy Markdown

No description provided.

@toh995

toh995 commented Jun 16, 2026

Copy link
Copy Markdown
Author

Not sure if I'll need to sign a CLA for this, or maybe a maintainer can update this for me?

Comment thread README.md
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.

Copy link
Copy Markdown
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This was the output I got when running the command, tested on cachyOS linux

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant