From c91ece4f58fffeb4ed987a9bb879e697ee132d28 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 4 Dec 2023 17:55:07 +0100 Subject: [PATCH] doc: typo Runnign (#3018) --- doc/dev/testing.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/dev/testing.md b/doc/dev/testing.md index b4ec0658a5..4de10edb3e 100644 --- a/doc/dev/testing.md +++ b/doc/dev/testing.md @@ -16,7 +16,7 @@ adding the `-C stageN` argument. The default when run as above is stage 1. The Lean tests will automatically use that stage's corresponding Lean executables -Runnign `make test` will not pick up new test files; run +Running `make test` will not pick up new test files; run ```bash cmake build/release/stage1 ```