From 65497649602ca5b56bed9418eda7d2e2be72487d Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 27 Jun 2022 22:11:09 -0400 Subject: [PATCH] typo --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index d7c50e9613fd..a7ee11e82e0f 100644 --- a/README.md +++ b/README.md @@ -277,7 +277,7 @@ environment variable. We first document the most relevant and most commonly used and `warn-nobacktrace` are the supported actions. The default is to `abort`, which halts the machine. Some (but not all) operations also support continuing execution with a "permission denied" error being returned to the program. - `warn` prints a full backtrace when that happen; `warn-nobacktrace` is less + `warn` prints a full backtrace when that happens; `warn-nobacktrace` is less verbose. `hide` hides the warning entirely. * `-Zmiri-env-exclude=` keeps the `var` environment variable isolated from the host so that it cannot be accessed by the program. Can be used multiple times to exclude several variables. The