FYI, I've just pushed this:
>From 29596f8db284a461933f2cff775bc65399f2efbc Mon Sep 17 00:00:00 2001
From: Jim Meyering <meyer...@fb.com>
Date: Tue, 19 Jun 2018 15:47:53 -0700
Subject: [PATCH] README-release: also run any check-very-expensive tests
* top/README-release: Adjust instructions so they run the
check-very-expensive tests when there is such a target.
---
ChangeLog | 6 ++++++
top/README-release | 5 +++--
2 files changed, 9 insertions(+), 2 deletions(-)
diff --git a/ChangeLog b/ChangeLog
index beaaf26a5..ac3fcab6a 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,9 @@
+2018-06-19 Jim Meyering <meyer...@fb.com>
+
+ README-release: also run any check-very-expensive tests
+ * top/README-release: Adjust instructions so they run the
+ check-very-expensive tests when there is such a target.
+
2018-06-18 Bruno Haible <br...@clisp.org>
pthread_rwlock_rdlock: Add comments regarding glibc behaviour.
diff --git a/top/README-release b/top/README-release
index a173203a1..536eef3a9 100644
--- a/top/README-release
+++ b/top/README-release
@@ -27,9 +27,10 @@ Here are most of the steps we (maintainers) follow when
making a release.
./bootstrap && ./configure
-* Pre-release testing: ensure that the following command succeeds:
+* Pre-release testing: ensure that the following commands succeed:
- make check syntax-check distcheck
+ c=check ve=check-very-expensive; git grep -q "^$ve:\$" && c=$ve
+ make $c syntax-check distcheck
* To (i) set the date, version number, and release TYPE on line 3 of
NEWS, (ii) commit that, and (iii) tag the release, run
--
