chore: remove comment from wrong stdlib_flags.h

This PR removes a comment from wrong `stdlib_flags.h`. Only the one in `stage0/` should be edited.
2026-04-06 04:04:06 +00:00 · 2025-12-09 15:44:13 +01:00
1 changed files with 0 additions and 2 deletions
--- 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;