From c2138827887da30124cfa1dc593cd6ec1d024a46 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 9 Dec 2025 15:58:30 +0100 Subject: [PATCH] chore: remove comment from wrong stdlib_flags.h (#11564) This PR removes a comment from wrong `stdlib_flags.h`. Only the one in `stage0/` should be edited. --- src/stdlib_flags.h | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h index 6c6b3bee8f..79a0e58edd 100644 --- a/src/stdlib_flags.h +++ b/src/stdlib_flags.h @@ -1,7 +1,5 @@ #include "util/options.h" -// update thy - namespace lean { options get_default_options() { options opts;