From 19c8ac834c4f43b1fd0c49aad286a4e5bebf0ce5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 28 May 2020 16:47:30 +0200
Subject: Adding missing DECLARE PLUGIN so that compilation with -natdynlink no
 works.

---
 user-contrib/Ltac2/g_ltac2.mlg | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'user-contrib')

diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 8979170026..3af39ec59a 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -8,6 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+DECLARE PLUGIN "ltac2_plugin"
+
 {
 
 open Pp
-- 
cgit v1.2.3