diff options
| author | Yves Bertot | 2018-05-04 16:04:54 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-04 16:04:54 +0200 |
| commit | cb20f241cc7ec686a5ae19c1e7b9eef6b26d230a (patch) | |
| tree | ec56b21410c26c23601b48890515a6eb6534014c /tuto0/src | |
| parent | eba06e2192d88af463fb6dec85e2f039a0a13694 (diff) | |
adds more packaging boilerplate in tuto0
Diffstat (limited to 'tuto0/src')
| -rw-r--r-- | tuto0/src/g_tuto0.ml4 | 4 | ||||
| -rw-r--r-- | tuto0/src/tuto0_main.ml | 1 | ||||
| -rw-r--r-- | tuto0/src/tuto0_main.mli | 1 | ||||
| -rw-r--r-- | tuto0/src/tuto0_plugin.mlpack | 1 |
4 files changed, 6 insertions, 1 deletions
diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4 index 5e0fa36e51..e3656fc986 100644 --- a/tuto0/src/g_tuto0.ml4 +++ b/tuto0/src/g_tuto0.ml4 @@ -1,5 +1,7 @@ +DECLARE PLUGIN "tuto0" + open Pp VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY -| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk "Hello World!") ] +| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk Tuto0_main.message) ] END
\ No newline at end of file diff --git a/tuto0/src/tuto0_main.ml b/tuto0/src/tuto0_main.ml new file mode 100644 index 0000000000..93a807a800 --- /dev/null +++ b/tuto0/src/tuto0_main.ml @@ -0,0 +1 @@ +let message = "Hello world!" diff --git a/tuto0/src/tuto0_main.mli b/tuto0/src/tuto0_main.mli new file mode 100644 index 0000000000..00d981ad75 --- /dev/null +++ b/tuto0/src/tuto0_main.mli @@ -0,0 +1 @@ +val message : string
\ No newline at end of file diff --git a/tuto0/src/tuto0_plugin.mlpack b/tuto0/src/tuto0_plugin.mlpack index 9360e6036e..02bc329591 100644 --- a/tuto0/src/tuto0_plugin.mlpack +++ b/tuto0/src/tuto0_plugin.mlpack @@ -1 +1,2 @@ +Tuto0_main G_tuto0
\ No newline at end of file |