diff --git a/src/Lean/Language/Lean.lean b/src/Lean/Language/Lean.lean
index a6f4cd269c..a88337274e 100644
--- a/src/Lean/Language/Lean.lean
+++ b/src/Lean/Language/Lean.lean
@@ -488,7 +488,7 @@ where
       let startTime := (← IO.monoNanosNow).toFloat / 1000000000
       let mut opts := setup.opts
       -- HACK: no better way to enable in core with `USE_LAKE` off
-      if setup.mainModuleName.getRoot ∈ [`Init, `Std, `Lean, `Lake] then
+      if setup.mainModuleName.getRoot ∈ [`Init, `Std, `Lean, `Lake, `LakeMain] then
         opts := experimental.module.setIfNotSet opts true
       if !stx.raw[0].isNone && !experimental.module.get opts then
         throw <| IO.Error.userError "`module` keyword is experimental and not enabled here"
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..cff0f06afc 100644
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// dear bot, please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;