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;