From 10ed2d489d8c8300f230aaccdcbdc6e54473d213 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Thu, 7 Apr 2022 00:49:05 +0100 Subject: [PATCH] update README --- README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 7c343a5..7e1f829 100644 --- a/README.md +++ b/README.md @@ -4,10 +4,10 @@ Document Generator for Lean 4 ## Usage You can call `doc-gen4` from the top of a Lake project like this: ```sh -$ /path/to/doc-gen4 / Module +$ /path/to/doc-gen4 Module ``` -Where the `/` is the root URL the HTML will refer to and `Module` is one or -more of the top level modules you want to document. + +where `Module` is one or more of the top level modules you want to document. The tool will then proceed to compile the project using lake (if that hasn't happened yet), analyze it and put the result in `./build/doc`. You could e.g. host the files locally with the built-in Python webserver: