From bcc012e553ded1855653dc6fbc15875749213f83 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Wed, 19 Aug 2020 15:14:07 -0400
Subject: Improve `make approve-output`

It now silently does nothing rather than erroring with `mv: cannot stat
'output/*.out.real': No such file or directory` if there is no output to
approve, and also correctly handles `output-coqtop` and `output-coqchk`
rather than ignoring these directories.

Fixes #12863
---
 .../11-infrastructure-and-dependencies/12864-fix-approve-output.rst  | 5 +++++
 1 file changed, 5 insertions(+)
 create mode 100644 doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst

(limited to 'doc')

diff --git a/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst b/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst
new file mode 100644
index 0000000000..c754826e62
--- /dev/null
+++ b/doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+  ``make approve-output`` in the test-suite now correctly handles
+  ``output-coqtop`` and ``output-coqchk`` tests (`#12864
+  <https://github.com/coq/coq/pull/12864>`_, fixes `#12863
+  <https://github.com/coq/coq/issues/12863>`_, by Jason Gross).
-- 
cgit v1.2.3