Unnamed repository; edit this file 'description' to name the repository.
Diffstat (limited to 'docs/user/generated_config.adoc')
| -rw-r--r-- | docs/user/generated_config.adoc | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/user/generated_config.adoc b/docs/user/generated_config.adoc index 2b518e0609..bd091db58d 100644 --- a/docs/user/generated_config.adoc +++ b/docs/user/generated_config.adoc @@ -95,7 +95,7 @@ avoid checking unnecessary things. Default: ---- [ - "debug_assertion", + "debug_assertions", "miri" ] ---- |