[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: src/Makefile unhelpful
From: |
Alan Mackenzie |
Subject: |
Re: src/Makefile unhelpful |
Date: |
Sat, 17 Sep 2022 11:20:40 +0000 |
Hello, Gregory.
On Sat, Sep 17, 2022 at 10:46:24 +0000, Gregory Heytings wrote:
> Complete patch attached, comments welcome.
Just a small point in English usage:
> I added a (minimal) sanity check, too. I remember at least one case when
> make "failed to fail", it returned 0 even though the build did in fact not
> succeed.
> +
> +# ADVICE-ON-FAILURE-BEGIN
> +# You might consider to:
> +# - run "make bootstrap", which might fix the problem
> +# - run "git clean -fdx" and run "make" again, which might fix
> +# the problem if it was not fixed by "make bootstrap"
> +# !BEWARE! "git clean -fdx" restores the local repository in its
> +# !BEWARE! pristine state, it deletes all local changes and all
> +# !BEWARE! untracked files
> +# - run "make V=1", which displays the full commandes invoked by
> +# make, to further investigate the problem
> +# ADVICE-ON-FAILURE-END
> +
The verb "consider" takes a gerund (or noun), not an infinitive. So the
above really ought to be:
You might consider:
- running ....
, with the other "run"s being changed to "running", too. Alternatively,
one could use instead the verb "try", which can take an infinitive (or a
gerund or noun ;-).
--
Alan Mackenzie (Nuremberg, Germany).
- Re: src/Makefile unhelpful, (continued)
- Re: src/Makefile unhelpful, Lars Ingebrigtsen, 2022/09/14
- Re: src/Makefile unhelpful, Gregory Heytings, 2022/09/14
- Re: src/Makefile unhelpful, Lars Ingebrigtsen, 2022/09/15
- Re: src/Makefile unhelpful, Gregory Heytings, 2022/09/15
- Re: src/Makefile unhelpful, Eli Zaretskii, 2022/09/15
- Re: src/Makefile unhelpful, Gregory Heytings, 2022/09/15
- Re: src/Makefile unhelpful, Eli Zaretskii, 2022/09/15
- Re: src/Makefile unhelpful, Óscar Fuentes, 2022/09/15
- Re: src/Makefile unhelpful, Gregory Heytings, 2022/09/15
- Re: src/Makefile unhelpful, Gregory Heytings, 2022/09/17
- Re: src/Makefile unhelpful,
Alan Mackenzie <=
- Re: src/Makefile unhelpful, Michael Welsh Duggan, 2022/09/17
- Re: src/Makefile unhelpful, Gregory Heytings, 2022/09/17
- Re: src/Makefile unhelpful, Gregory Heytings, 2022/09/17
- Re: src/Makefile unhelpful, Lars Ingebrigtsen, 2022/09/18
- Re: src/Makefile unhelpful, Gerd Möllmann, 2022/09/18
- Re: src/Makefile unhelpful, Andreas Schwab, 2022/09/18
- Re: src/Makefile unhelpful, Gerd Möllmann, 2022/09/18
- Re: src/Makefile unhelpful, Robert Pluim, 2022/09/18
- Re: src/Makefile unhelpful, Gregory Heytings, 2022/09/18
- Re: src/Makefile unhelpful, Andreas Schwab, 2022/09/18