diff options
| author | Gaëtan Gilbert | 2020-08-24 13:49:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-08-24 13:49:20 +0200 |
| commit | f42b28ed0cfd200395a4a32fd1ebe6a7f73a7ddb (patch) | |
| tree | 540e542c5e34d228e7ae4a55ac9c743a90d6328d /doc | |
| parent | 99e944f873589cf350e49f3bfda6094ffbfa545b (diff) | |
| parent | bcc012e553ded1855653dc6fbc15875749213f83 (diff) | |
Merge PR #12864: Improve `make approve-output`
Reviewed-by: SkySkimmer
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/11-infrastructure-and-dependencies/12864-fix-approve-output.rst | 5 |
1 files changed, 5 insertions, 0 deletions
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). |