From 40ec83362336cfc1009ca4c17ea2aa015def5df4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 12 Dec 2021 13:27:38 +0100
Subject: [PATCH] doc: Basic usage in README

---
 README.md | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/README.md b/README.md
index fcf7a8a..d0ff1e1 100644
--- a/README.md
+++ b/README.md
@@ -1,2 +1,15 @@
 # doc-gen4
 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
+```
+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:
+```sh
+$ cd build/doc && python -m http.server
+```