On Thu, 10 Oct 2019 16:51:56 +0000, Carl Sorensen <c_soren...@byu.edu> wrote:
> Given that make will not do anything if the source tree has not been changed, > I see no problem (and plenty of benefit) in having make check do the > equivalent of make && make check. > > Personally, however, I prefer to do > > make > make check > > rather than > > make && make check Yes. Especially with testing patches. Sometimes a developer submits a patch without doing basic make (or they end up submitting a patch from their 'own' tree that breaks make on current master), so having two distinct make commands helps me help them determine the patch error. (if that is where we were going with this). James _______________________________________________ lilypond-devel mailing list lilypond-devel@gnu.org https://lists.gnu.org/mailman/listinfo/lilypond-devel
