aboutsummaryrefslogtreecommitdiff
path: root/tuto0/src/g_tuto0.ml4
blob: e3656fc9862be506c3d452746b9f173eb5fed03d (plain)
1
2
3
4
5
6
7
DECLARE PLUGIN "tuto0"

open Pp

VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk Tuto0_main.message) ]
END