From 712231dcda4eb6b6fe37927f304df48d7595ffe5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Feb 2025 09:39:17 -0800 Subject: [PATCH] fix #7560 --- src/cmd_context/basic_cmds.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index 8db1a615d..ff74e4614 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -737,6 +737,7 @@ public: else { if (opt != symbol(":?")) ctx.print_unsupported(opt, m_line, m_pos); + ctx.regular_stream() << "; Suppported get-info parameters:\n"; ctx.regular_stream() << "; (get-info :reason-unknown)\n"; ctx.regular_stream() << "; (get-info :status)\n"; ctx.regular_stream() << "; (get-info :version)\n";