chore: request update stage0

feat: expose optionValue parser
2026-03-23 21:34:10 +00:00 · 2025-10-19 15:33:57 -07:00 · 2025-10-19 15:33:26 -07:00
2 changed files with 10 additions and 8 deletions
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -909,14 +909,15 @@ abbrev declModifiersT := declModifiers true
 builtin_initialize
  register_parser_alias (kind := ``declModifiers) "declModifiers"       declModifiersF
  register_parser_alias (kind := ``declModifiers) "nestedDeclModifiers" declModifiersT
-  register_parser_alias                                                 declId
-  register_parser_alias                                                 declSig
-  register_parser_alias                                                 declVal
-  register_parser_alias                                                 optDeclSig
-  register_parser_alias                                                 openDecl
-  register_parser_alias                                                 docComment
-  register_parser_alias                                                 plainDocComment
-  register_parser_alias                                                 visibility
+  register_parser_alias declId
+  register_parser_alias declSig
+  register_parser_alias declVal
+  register_parser_alias optDeclSig
+  register_parser_alias openDecl
+  register_parser_alias docComment
+  register_parser_alias plainDocComment
+  register_parser_alias visibility
+  register_parser_alias "optionValue" Command.optionValue

 /--
 Registers an error explanation.
--- a/stage0/src/stdlib_flags.h
+++ b/stage0/src/stdlib_flags.h
@@ -1,3 +1,4 @@
+// update me!
 #include "util/options.h"

 namespace lean {
Author	SHA1	Message	Date
Leonardo de Moura	36cd28af98	chore: request update stage0	2025-10-19 15:33:57 -07:00
Leonardo de Moura	aed91a9efd	feat: expose `optionValue` parser	2025-10-19 15:33:26 -07:00