From 2ab7948163863ee222891653ac98941fe4f20e87 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 14 Mar 2024 16:26:27 +1100
Subject: [PATCH] cleanup README

---
 README.md | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/README.md b/README.md
index e6ba2f3..d6adc28 100644
--- a/README.md
+++ b/README.md
@@ -61,7 +61,7 @@ showing any messages generated, and sorries with their goal states.
 
 There is a simple wrapper around command mode that allows reading in an entire file.
 
-If `file.lean` contains
+If `test/file.lean` contains
 ```lean
 def f : Nat := 37
 
@@ -70,11 +70,11 @@ def g := 2
 theorem h : f + g = 39 := by exact rfl
 ```
 
-then sending
-```json
-{"path": "test/file.lean", "allTactics": true}
+then
+```
+echo '{"path": "test/file.lean", "allTactics": true}' | lake exe repl
 ```
-to the REPL results in output
+results in output
 ```json
 {"tactics":
  [{"tactic": "exact rfl",