From 6bc9ef56c5833ee81d7298ab0c52146ad775e2a1 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 2 Aug 2019 16:47:49 +0200
Subject: Make sure that all query commands return a notice (not an info)
 feedback

As documented in the feedback API.
---
 test-suite/output/auto.out | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
index 2761b87b02..5e81b43504 100644
--- a/test-suite/output/auto.out
+++ b/test-suite/output/auto.out
@@ -2,18 +2,18 @@
 simple apply or_intror (in core).
  intro.
  assumption.
-Debug: (* debug auto: *)
-Debug: * assumption. (*fail*)
-Debug: * intro. (*fail*)
-Debug: * simple apply or_intror (in core). (*success*)
-Debug: ** assumption. (*fail*)
-Debug: ** intro. (*success*)
-Debug: ** assumption. (*success*)
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+* simple apply or_intror (in core). (*success*)
+** assumption. (*fail*)
+** intro. (*success*)
+** assumption. (*success*)
 (* info eauto: *)
 simple apply or_intror.
  intro.
  exact H.
-Debug: (* debug eauto: *)
+(* debug eauto: *)
 Debug: 1 depth=5 
 Debug: 1.1 depth=4 simple apply or_intror
 Debug: 1.1.1 depth=4 intro
-- 
cgit v1.2.3