< Press Enter to see the Survival Guide >
parent
7159474be3
commit
7c6e67b5ec
|
@ -379,12 +379,16 @@ interactor "completion" f {
|
||||||
{ T{ key-down f { C+ } "r" } history-completion-popup }
|
{ T{ key-down f { C+ } "r" } history-completion-popup }
|
||||||
} define-command-map
|
} define-command-map
|
||||||
|
|
||||||
|
: introduction. ( -- )
|
||||||
|
tip-of-the-day. nl
|
||||||
|
{ $strong "Press " { $snippet "F1" } " at any time for help." } print-content nl nl ;
|
||||||
|
|
||||||
: listener-thread ( listener -- )
|
: listener-thread ( listener -- )
|
||||||
dup listener-streams [
|
dup listener-streams [
|
||||||
[ com-browse ] help-hook set
|
[ com-browse ] help-hook set
|
||||||
'[ [ _ input>> ] 2dip debugger-popup ] error-hook set
|
'[ [ _ input>> ] 2dip debugger-popup ] error-hook set
|
||||||
error-summary? off
|
error-summary? off
|
||||||
tip-of-the-day. nl
|
introduction.
|
||||||
listener
|
listener
|
||||||
nl
|
nl
|
||||||
"The listener has exited. To start it again, click “Restart Listener”." print
|
"The listener has exited. To start it again, click “Restart Listener”." print
|
||||||
|
|
Loading…
Reference in New Issue