summaryrefslogtreecommitdiff
path: root/top
diff options
context:
space:
mode:
authorJim Meyering <meyering@fb.com>2018-06-19 15:47:53 -0700
committerJim Meyering <meyering@fb.com>2018-06-19 15:47:53 -0700
commit29596f8db284a461933f2cff775bc65399f2efbc (patch)
treeab2cafcaf4b3d81879db9b985aebde588d7f8c91 /top
parent5288100a985833560d9fb03a32d702296e660b06 (diff)
downloadgnulib-29596f8db284a461933f2cff775bc65399f2efbc.tar.gz
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.
Diffstat (limited to 'top')
-rw-r--r--top/README-release5
1 files changed, 3 insertions, 2 deletions
diff --git a/top/README-release b/top/README-release
index a173203a1f..536eef3a9f 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