From b88102233366b9290fc8819443764a15c109e00c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 17 May 2018 17:23:21 +0200
Subject: DECLARE PLUGIN "$name" === Declare ML Module "$name"

---
 tuto0/src/g_tuto0.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4
index df6e187d52..d6e95ba0f7 100644
--- a/tuto0/src/g_tuto0.ml4
+++ b/tuto0/src/g_tuto0.ml4
@@ -1,4 +1,4 @@
-DECLARE PLUGIN "tuto0"
+DECLARE PLUGIN "tuto0_plugin"
 
 open Pp
 open Ltac_plugin
-- 
cgit v1.2.3