Re: [PATCH] add a script to diff rendered documentation

From: brian m. carlson <sandals@crustytoothpaste.net>
Date: Aug 5, 2018, 20:49 UTC
Message-ID: <20180805204930.GA202464@genre.crustytoothpaste.net>
In-Reply-To: <20180803205204.GA3790@sigill.intra.peff.net>

On Fri, Aug 03, 2018 at 04:52:05PM -0400, Jeff King wrote:

Show 5 quoted lines

> I wrote this up for my own use after our discussion in [1]. I'm not sure
> if it's too ugly for inclusion, or if it might be helpful to others.
> I've only just written it, but my plan is to try to run it on anything I
> submit to check the formatting. So it _seems_ useful and appears to
> work, but only after a few minutes of playing with it. :)

I think this would indeed be valuable. Junio seemed to indicate that he would use it, and I would certainly use it as well.

Show 18 quoted lines

> diff --git a/Documentation/doc-diff b/Documentation/doc-diff
> new file mode 100755
> index 0000000000..61deb2579e
> --- /dev/null
> +++ b/Documentation/doc-diff
> @@ -0,0 +1,100 @@
> +#!/bin/sh
> +
> +OPTIONS_SPEC="\
> +doc-diff <from> <to> [-- diff options]
> +--
> +j	parallel argument to pass to make
> +f	force rebuild; do not rely on cached results
> +"
> +SUBDIRECTORY_OK=1
> +. "$(git --exec-path)/git-sh-setup"
> +
> +parallel=8

I'm not sure -j8 is a great default. There are still a lot of two-core/four-thread machines out there, such as my laptop (from 2016). Maybe we should default this to 1 unless -j is provided, like make does.

-- 
brian m. carlson: Houston, Texas, US
OpenPGP: https://keybase.io/bk2204