diff options
| author | Maxime Dénès | 2019-08-02 16:47:49 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-08-29 10:27:04 +0200 |
| commit | 6bc9ef56c5833ee81d7298ab0c52146ad775e2a1 (patch) | |
| tree | 8ea8af9ee03d627126de323898ce73d3a43e608e /test-suite | |
| parent | 1e6fb6005ef98d1709b09adfcb0726da2fc8b7f4 (diff) | |
Make sure that all query commands return a notice (not an info) feedback
As documented in the feedback API.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/output/auto.out | 16 |
1 files changed, 8 insertions, 8 deletions
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 |