diff options
author | Jim Meyering <meyering@fb.com> | 2018-06-19 15:47:53 -0700 |
---|---|---|
committer | Jim Meyering <meyering@fb.com> | 2018-06-19 15:47:53 -0700 |
commit | 29596f8db284a461933f2cff775bc65399f2efbc (patch) | |
tree | ab2cafcaf4b3d81879db9b985aebde588d7f8c91 /top/README-release | |
parent | 5288100a985833560d9fb03a32d702296e660b06 (diff) | |
download | gnulib-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/README-release')
-rw-r--r-- | top/README-release | 5 |
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 |