From 4b406b6d5ffd5f759fc2c49a0ba786f1d33fbeb7 Mon Sep 17 00:00:00 2001
From: jrr6 <7482866+jrr6@users.noreply.github.com>
Date: Mon, 17 Mar 2025 14:07:58 -0400
Subject: [PATCH] chore: remove comment from `src/stdlib_flags.h` (#7531)

This PR removes a misplaced comment from `src/stdlib_flags.h` introduced
by #7425 that was intended to (ephemerally) go in
`stage0/src/stdlib_flags.h`.
---
 src/stdlib_flags.h | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/stdlib_flags.h b/src/stdlib_flags.h
index ee225c1734..b647d85f37 100644
--- a/src/stdlib_flags.h
+++ b/src/stdlib_flags.h
@@ -1,7 +1,5 @@
 #include "util/options.h"
 
-// update stage0
-
 namespace lean {
 options get_default_options() {
     options opts;