From a7b406bccfd51d7afee1f26ecfe38002be3b76f2 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 7 Feb 2019 08:06:20 +0100
Subject: Fix Locate printing regression

Fixes #9428. (Again.)

This is a cherry-pick of 68927ac4/4b02fbd9 bugfixes, because 0251c800 reverted them.
Corrects a 8.9.1 → 8.10.0 regression.

(cherry picked from commit 68927ac48b1ce8fe30edef24defdcdc84173a5a5)
---
 test-suite/output/locate.out | 3 +++
 test-suite/output/locate.v   | 3 +++
 2 files changed, 6 insertions(+)
 create mode 100644 test-suite/output/locate.out
 create mode 100644 test-suite/output/locate.v

(limited to 'test-suite')

diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
new file mode 100644
index 0000000000..473db2d312
--- /dev/null
+++ b/test-suite/output/locate.out
@@ -0,0 +1,3 @@
+Notation
+"b1 && b2" := if b1 then b2 else false (default interpretation)
+"x && y" := andb x y : bool_scope
diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v
new file mode 100644
index 0000000000..af8b0ee193
--- /dev/null
+++ b/test-suite/output/locate.v
@@ -0,0 +1,3 @@
+Set Printing Width 400.
+Notation "b1 && b2" := (if b1 then b2 else false).
+Locate "&&".
-- 
cgit v1.2.3