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.

Author: nomeata

src/stdlib_flags.h

@@ -1,7 +1,5 @@
 #include "util/options.h"
 
-// update thy
-
 namespace lean {
 options get_default_options() {
     options opts;