From cb20f241cc7ec686a5ae19c1e7b9eef6b26d230a Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 16:04:54 +0200
Subject: adds more packaging boilerplate in tuto0

---
 tuto0/src/g_tuto0.ml4         | 4 +++-
 tuto0/src/tuto0_main.ml       | 1 +
 tuto0/src/tuto0_main.mli      | 1 +
 tuto0/src/tuto0_plugin.mlpack | 1 +
 4 files changed, 6 insertions(+), 1 deletion(-)
 create mode 100644 tuto0/src/tuto0_main.ml
 create mode 100644 tuto0/src/tuto0_main.mli

(limited to 'tuto0/src')

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
-- 
cgit v1.2.3