From 51727bae4bb4650d7fa297b983fdc13608ae6e17 Mon Sep 17 00:00:00 2001 From: zachs18 <8355914+zachs18@users.noreply.github.com> Date: Sun, 7 Jul 2024 11:23:13 -0500 Subject: [PATCH] Update src/bootstrap/mk/Makefile.in Co-authored-by: Ralf Jung --- src/bootstrap/mk/Makefile.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/bootstrap/mk/Makefile.in b/src/bootstrap/mk/Makefile.in index 6267156e8e25..3d977bf30586 100644 --- a/src/bootstrap/mk/Makefile.in +++ b/src/bootstrap/mk/Makefile.in @@ -58,7 +58,7 @@ check-aux: library/core \ library/alloc \ --no-doc - # Some use file system operations to demonstrate dealing with `Result`. + # Some doctests use file system operations to demonstrate dealing with `Result`. $(Q)MIRIFLAGS="-Zmiri-disable-isolation" \ $(BOOTSTRAP) miri --stage 2 \ library/core \