From 72e6699279ac7ce2499405d64d524530789c8f58 Mon Sep 17 00:00:00 2001 From: Alexander Iljin Date: Sun, 14 May 2017 19:57:18 +0300 Subject: [PATCH] ui.tools.listener-docs: wrap a hotkey in the $snippet tag --- basis/ui/tools/listener/listener-docs.factor | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/basis/ui/tools/listener/listener-docs.factor b/basis/ui/tools/listener/listener-docs.factor index d5bd19366a..5626e4fa69 100644 --- a/basis/ui/tools/listener/listener-docs.factor +++ b/basis/ui/tools/listener/listener-docs.factor @@ -97,6 +97,6 @@ TIP: "Scroll the listener from the keyboard by pressing " { $command listener-ga TIP: "Press " { $command tool "common" refresh-all } " or run " { $link refresh-all } " to reload changed source files from disk." ; -TIP: "On Windows: use C+Break to interrupt tight loops in your code started in the listener, such as" { $code "[ t ] [ ] while" } "Caution: this may crash the Factor runtime if the code uses cooperative multitasking or asynchronous I/O." ; +TIP: "On Windows: use " { $snippet "C+Break" } " to interrupt tight loops in your code started in the listener, such as" { $code "[ t ] [ ] while" } "Caution: this may crash the Factor runtime if the code uses cooperative multitasking or asynchronous I/O." ; ABOUT: "ui-listener"