From dd8d2a1d017d20635f943af205dcb0127a992a59 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 29 Jun 2016 08:13:32 +0200
Subject: Fix issues in test-suite revealed by warnings.

---
 test-suite/bugs/closed/3251.v | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test-suite/bugs')

diff --git a/test-suite/bugs/closed/3251.v b/test-suite/bugs/closed/3251.v
index 5a7ae2002b..d4ce050c57 100644
--- a/test-suite/bugs/closed/3251.v
+++ b/test-suite/bugs/closed/3251.v
@@ -1,4 +1,5 @@
 Goal True.
+idtac.
 Ltac foo := idtac.
 (* print out happens twice:
 foo is defined
-- 
cgit v1.2.3